(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x_0_0 () Bool)
(declare-fun x_0_1 () Bool)
(declare-fun x_0_2 () Bool)
(declare-fun x_1_0 () Bool)
(declare-fun x_1_1 () Bool)
(declare-fun x_1_2 () Bool)
(declare-fun x_2_0 () Bool)
(declare-fun x_2_1 () Bool)
(declare-fun x_2_2 () Bool)
(declare-fun x_3_0 () Bool)
(declare-fun x_3_1 () Bool)
(declare-fun x_3_2 () Bool)
(declare-fun x_4_0 () Bool)
(declare-fun x_4_1 () Bool)
(declare-fun x_4_2 () Bool)
(declare-fun x_5_0 () Bool)
(declare-fun x_5_1 () Bool)
(declare-fun x_5_2 () Bool)
(declare-fun x_6_0 () Bool)
(declare-fun x_6_1 () Bool)
(declare-fun x_6_2 () Bool)
(declare-fun x_7_0 () Bool)
(declare-fun x_7_1 () Bool)
(declare-fun x_7_2 () Bool)
(declare-fun x_8_0 () Bool)
(declare-fun x_8_1 () Bool)
(declare-fun x_8_2 () Bool)
(declare-fun x_9_0 () Bool)
(declare-fun x_9_1 () Bool)
(declare-fun x_9_2 () Bool)
(declare-fun x_10_0 () Bool)
(declare-fun x_10_1 () Bool)
(declare-fun x_10_2 () Bool)
(declare-fun x_11_0 () Bool)
(declare-fun x_11_1 () Bool)
(declare-fun x_11_2 () Bool)
(declare-fun x_12_0 () Bool)
(declare-fun x_12_1 () Bool)
(declare-fun x_12_2 () Bool)
(declare-fun x_13_0 () Bool)
(declare-fun x_13_1 () Bool)
(declare-fun x_13_2 () Bool)
(declare-fun x_14_0 () Bool)
(declare-fun x_14_1 () Bool)
(declare-fun x_14_2 () Bool)
(declare-fun x_15_0 () Bool)
(declare-fun x_15_1 () Bool)
(declare-fun x_15_2 () Bool)
(declare-fun x_16_0 () Bool)
(declare-fun x_16_1 () Bool)
(declare-fun x_16_2 () Bool)
(declare-fun x_17_0 () Bool)
(declare-fun x_17_1 () Bool)
(declare-fun x_17_2 () Bool)
(declare-fun x_18_0 () Bool)
(declare-fun x_18_1 () Bool)
(declare-fun x_18_2 () Bool)
(declare-fun x_19_0 () Bool)
(declare-fun x_19_1 () Bool)
(declare-fun x_19_2 () Bool)
(declare-fun x_20_0 () Bool)
(declare-fun x_20_1 () Bool)
(declare-fun x_20_2 () Bool)
(declare-fun x_21_0 () Bool)
(declare-fun x_21_1 () Bool)
(declare-fun x_21_2 () Bool)
(declare-fun x_22_0 () Bool)
(declare-fun x_22_1 () Bool)
(declare-fun x_22_2 () Bool)
(declare-fun x_23_0 () Bool)
(declare-fun x_23_1 () Bool)
(declare-fun x_23_2 () Bool)
(declare-fun x_24_0 () Bool)
(declare-fun x_24_1 () Bool)
(declare-fun x_24_2 () Bool)
(declare-fun x_25_0 () Bool)
(declare-fun x_25_1 () Bool)
(declare-fun x_25_2 () Bool)
(declare-fun x_26_0 () Bool)
(declare-fun x_26_1 () Bool)
(declare-fun x_26_2 () Bool)
(declare-fun x_27_0 () Bool)
(declare-fun x_27_1 () Bool)
(declare-fun x_27_2 () Bool)
(declare-fun x_28_0 () Bool)
(declare-fun x_28_1 () Bool)
(declare-fun x_28_2 () Bool)
(declare-fun x_29_0 () Bool)
(declare-fun x_29_1 () Bool)
(declare-fun x_29_2 () Bool)
(declare-fun x_30_0 () Bool)
(declare-fun x_30_1 () Bool)
(declare-fun x_30_2 () Bool)
(declare-fun x_31_0 () Bool)
(declare-fun x_31_1 () Bool)
(declare-fun x_31_2 () Bool)
(declare-fun x_32_0 () Bool)
(declare-fun x_32_1 () Bool)
(declare-fun x_32_2 () Bool)
(declare-fun x_33_0 () Bool)
(declare-fun x_33_1 () Bool)
(declare-fun x_33_2 () Bool)
(declare-fun x_34_0 () Bool)
(declare-fun x_34_1 () Bool)
(declare-fun x_34_2 () Bool)
(declare-fun x_35_0 () Bool)
(declare-fun x_35_1 () Bool)
(declare-fun x_35_2 () Bool)
(declare-fun x_36_0 () Bool)
(declare-fun x_36_1 () Bool)
(declare-fun x_36_2 () Bool)
(declare-fun x_37_0 () Bool)
(declare-fun x_37_1 () Bool)
(declare-fun x_37_2 () Bool)
(declare-fun x_38_0 () Bool)
(declare-fun x_38_1 () Bool)
(declare-fun x_38_2 () Bool)
(declare-fun x_39_0 () Bool)
(declare-fun x_39_1 () Bool)
(declare-fun x_39_2 () Bool)
(declare-fun a_0_0 () U)
(declare-fun a_0_1 () U)
(declare-fun a_0_2 () U)
(declare-fun a_0_3 () U)
(declare-fun a_0_4 () U)
(declare-fun a_0_5 () U)
(declare-fun a_0_6 () U)
(declare-fun a_0_7 () U)
(declare-fun a_0_8 () U)
(declare-fun a_0_9 () U)
(declare-fun a_0_10 () U)
(declare-fun a_0_11 () U)
(declare-fun a_0_12 () U)
(declare-fun a_0_13 () U)
(declare-fun a_0_14 () U)
(declare-fun a_0_15 () U)
(declare-fun a_0_16 () U)
(declare-fun a_0_17 () U)
(declare-fun a_0_18 () U)
(declare-fun a_0_19 () U)
(declare-fun a_0_20 () U)
(declare-fun a_0_21 () U)
(declare-fun a_0_22 () U)
(declare-fun a_0_23 () U)
(declare-fun a_0_24 () U)
(declare-fun a_0_25 () U)
(declare-fun a_0_26 () U)
(declare-fun a_0_27 () U)
(declare-fun a_0_28 () U)
(declare-fun a_0_29 () U)
(declare-fun a_0_30 () U)
(declare-fun a_0_31 () U)
(declare-fun a_0_32 () U)
(declare-fun a_0_33 () U)
(declare-fun a_0_34 () U)
(declare-fun a_0_35 () U)
(declare-fun a_0_36 () U)
(declare-fun a_0_37 () U)
(declare-fun a_0_38 () U)
(declare-fun a_0_39 () U)
(declare-fun a_1_0 () U)
(declare-fun a_1_1 () U)
(declare-fun a_1_2 () U)
(declare-fun a_1_3 () U)
(declare-fun a_1_4 () U)
(declare-fun a_1_5 () U)
(declare-fun a_1_6 () U)
(declare-fun a_1_7 () U)
(declare-fun a_1_8 () U)
(declare-fun a_1_9 () U)
(declare-fun a_1_10 () U)
(declare-fun a_1_11 () U)
(declare-fun a_1_12 () U)
(declare-fun a_1_13 () U)
(declare-fun a_1_14 () U)
(declare-fun a_1_15 () U)
(declare-fun a_1_16 () U)
(declare-fun a_1_17 () U)
(declare-fun a_1_18 () U)
(declare-fun a_1_19 () U)
(declare-fun a_1_20 () U)
(declare-fun a_1_21 () U)
(declare-fun a_1_22 () U)
(declare-fun a_1_23 () U)
(declare-fun a_1_24 () U)
(declare-fun a_1_25 () U)
(declare-fun a_1_26 () U)
(declare-fun a_1_27 () U)
(declare-fun a_1_28 () U)
(declare-fun a_1_29 () U)
(declare-fun a_1_30 () U)
(declare-fun a_1_31 () U)
(declare-fun a_1_32 () U)
(declare-fun a_1_33 () U)
(declare-fun a_1_34 () U)
(declare-fun a_1_35 () U)
(declare-fun a_1_36 () U)
(declare-fun a_1_37 () U)
(declare-fun a_1_38 () U)
(declare-fun a_1_39 () U)
(declare-fun a_2_0 () U)
(declare-fun a_2_1 () U)
(declare-fun a_2_2 () U)
(declare-fun a_2_3 () U)
(declare-fun a_2_4 () U)
(declare-fun a_2_5 () U)
(declare-fun a_2_6 () U)
(declare-fun a_2_7 () U)
(declare-fun a_2_8 () U)
(declare-fun a_2_9 () U)
(declare-fun a_2_10 () U)
(declare-fun a_2_11 () U)
(declare-fun a_2_12 () U)
(declare-fun a_2_13 () U)
(declare-fun a_2_14 () U)
(declare-fun a_2_15 () U)
(declare-fun a_2_16 () U)
(declare-fun a_2_17 () U)
(declare-fun a_2_18 () U)
(declare-fun a_2_19 () U)
(declare-fun a_2_20 () U)
(declare-fun a_2_21 () U)
(declare-fun a_2_22 () U)
(declare-fun a_2_23 () U)
(declare-fun a_2_24 () U)
(declare-fun a_2_25 () U)
(declare-fun a_2_26 () U)
(declare-fun a_2_27 () U)
(declare-fun a_2_28 () U)
(declare-fun a_2_29 () U)
(declare-fun a_2_30 () U)
(declare-fun a_2_31 () U)
(declare-fun a_2_32 () U)
(declare-fun a_2_33 () U)
(declare-fun a_2_34 () U)
(declare-fun a_2_35 () U)
(declare-fun a_2_36 () U)
(declare-fun a_2_37 () U)
(declare-fun a_2_38 () U)
(declare-fun a_2_39 () U)
(declare-fun a_3_0 () U)
(declare-fun a_3_1 () U)
(declare-fun a_3_2 () U)
(declare-fun a_3_3 () U)
(declare-fun a_3_4 () U)
(declare-fun a_3_5 () U)
(declare-fun a_3_6 () U)
(declare-fun a_3_7 () U)
(declare-fun a_3_8 () U)
(declare-fun a_3_9 () U)
(declare-fun a_3_10 () U)
(declare-fun a_3_11 () U)
(declare-fun a_3_12 () U)
(declare-fun a_3_13 () U)
(declare-fun a_3_14 () U)
(declare-fun a_3_15 () U)
(declare-fun a_3_16 () U)
(declare-fun a_3_17 () U)
(declare-fun a_3_18 () U)
(declare-fun a_3_19 () U)
(declare-fun a_3_20 () U)
(declare-fun a_3_21 () U)
(declare-fun a_3_22 () U)
(declare-fun a_3_23 () U)
(declare-fun a_3_24 () U)
(declare-fun a_3_25 () U)
(declare-fun a_3_26 () U)
(declare-fun a_3_27 () U)
(declare-fun a_3_28 () U)
(declare-fun a_3_29 () U)
(declare-fun a_3_30 () U)
(declare-fun a_3_31 () U)
(declare-fun a_3_32 () U)
(declare-fun a_3_33 () U)
(declare-fun a_3_34 () U)
(declare-fun a_3_35 () U)
(declare-fun a_3_36 () U)
(declare-fun a_3_37 () U)
(declare-fun a_3_38 () U)
(declare-fun a_3_39 () U)
(declare-fun a_4_0 () U)
(declare-fun a_4_1 () U)
(declare-fun a_4_2 () U)
(declare-fun a_4_3 () U)
(declare-fun a_4_4 () U)
(declare-fun a_4_5 () U)
(declare-fun a_4_6 () U)
(declare-fun a_4_7 () U)
(declare-fun a_4_8 () U)
(declare-fun a_4_9 () U)
(declare-fun a_4_10 () U)
(declare-fun a_4_11 () U)
(declare-fun a_4_12 () U)
(declare-fun a_4_13 () U)
(declare-fun a_4_14 () U)
(declare-fun a_4_15 () U)
(declare-fun a_4_16 () U)
(declare-fun a_4_17 () U)
(declare-fun a_4_18 () U)
(declare-fun a_4_19 () U)
(declare-fun a_4_20 () U)
(declare-fun a_4_21 () U)
(declare-fun a_4_22 () U)
(declare-fun a_4_23 () U)
(declare-fun a_4_24 () U)
(declare-fun a_4_25 () U)
(declare-fun a_4_26 () U)
(declare-fun a_4_27 () U)
(declare-fun a_4_28 () U)
(declare-fun a_4_29 () U)
(declare-fun a_4_30 () U)
(declare-fun a_4_31 () U)
(declare-fun a_4_32 () U)
(declare-fun a_4_33 () U)
(declare-fun a_4_34 () U)
(declare-fun a_4_35 () U)
(declare-fun a_4_36 () U)
(declare-fun a_4_37 () U)
(declare-fun a_4_38 () U)
(declare-fun a_4_39 () U)
(declare-fun a_5_0 () U)
(declare-fun a_5_1 () U)
(declare-fun a_5_2 () U)
(declare-fun a_5_3 () U)
(declare-fun a_5_4 () U)
(declare-fun a_5_5 () U)
(declare-fun a_5_6 () U)
(declare-fun a_5_7 () U)
(declare-fun a_5_8 () U)
(declare-fun a_5_9 () U)
(declare-fun a_5_10 () U)
(declare-fun a_5_11 () U)
(declare-fun a_5_12 () U)
(declare-fun a_5_13 () U)
(declare-fun a_5_14 () U)
(declare-fun a_5_15 () U)
(declare-fun a_5_16 () U)
(declare-fun a_5_17 () U)
(declare-fun a_5_18 () U)
(declare-fun a_5_19 () U)
(declare-fun a_5_20 () U)
(declare-fun a_5_21 () U)
(declare-fun a_5_22 () U)
(declare-fun a_5_23 () U)
(declare-fun a_5_24 () U)
(declare-fun a_5_25 () U)
(declare-fun a_5_26 () U)
(declare-fun a_5_27 () U)
(declare-fun a_5_28 () U)
(declare-fun a_5_29 () U)
(declare-fun a_5_30 () U)
(declare-fun a_5_31 () U)
(declare-fun a_5_32 () U)
(declare-fun a_5_33 () U)
(declare-fun a_5_34 () U)
(declare-fun a_5_35 () U)
(declare-fun a_5_36 () U)
(declare-fun a_5_37 () U)
(declare-fun a_5_38 () U)
(declare-fun a_5_39 () U)
(declare-fun a_6_0 () U)
(declare-fun a_6_1 () U)
(declare-fun a_6_2 () U)
(declare-fun a_6_3 () U)
(declare-fun a_6_4 () U)
(declare-fun a_6_5 () U)
(declare-fun a_6_6 () U)
(declare-fun a_6_7 () U)
(declare-fun a_6_8 () U)
(declare-fun a_6_9 () U)
(declare-fun a_6_10 () U)
(declare-fun a_6_11 () U)
(declare-fun a_6_12 () U)
(declare-fun a_6_13 () U)
(declare-fun a_6_14 () U)
(declare-fun a_6_15 () U)
(declare-fun a_6_16 () U)
(declare-fun a_6_17 () U)
(declare-fun a_6_18 () U)
(declare-fun a_6_19 () U)
(declare-fun a_6_20 () U)
(declare-fun a_6_21 () U)
(declare-fun a_6_22 () U)
(declare-fun a_6_23 () U)
(declare-fun a_6_24 () U)
(declare-fun a_6_25 () U)
(declare-fun a_6_26 () U)
(declare-fun a_6_27 () U)
(declare-fun a_6_28 () U)
(declare-fun a_6_29 () U)
(declare-fun a_6_30 () U)
(declare-fun a_6_31 () U)
(declare-fun a_6_32 () U)
(declare-fun a_6_33 () U)
(declare-fun a_6_34 () U)
(declare-fun a_6_35 () U)
(declare-fun a_6_36 () U)
(declare-fun a_6_37 () U)
(declare-fun a_6_38 () U)
(declare-fun a_6_39 () U)
(declare-fun a_7_0 () U)
(declare-fun a_7_1 () U)
(declare-fun a_7_2 () U)
(declare-fun a_7_3 () U)
(declare-fun a_7_4 () U)
(declare-fun a_7_5 () U)
(declare-fun a_7_6 () U)
(declare-fun a_7_7 () U)
(declare-fun a_7_8 () U)
(declare-fun a_7_9 () U)
(declare-fun a_7_10 () U)
(declare-fun a_7_11 () U)
(declare-fun a_7_12 () U)
(declare-fun a_7_13 () U)
(declare-fun a_7_14 () U)
(declare-fun a_7_15 () U)
(declare-fun a_7_16 () U)
(declare-fun a_7_17 () U)
(declare-fun a_7_18 () U)
(declare-fun a_7_19 () U)
(declare-fun a_7_20 () U)
(declare-fun a_7_21 () U)
(declare-fun a_7_22 () U)
(declare-fun a_7_23 () U)
(declare-fun a_7_24 () U)
(declare-fun a_7_25 () U)
(declare-fun a_7_26 () U)
(declare-fun a_7_27 () U)
(declare-fun a_7_28 () U)
(declare-fun a_7_29 () U)
(declare-fun a_7_30 () U)
(declare-fun a_7_31 () U)
(declare-fun a_7_32 () U)
(declare-fun a_7_33 () U)
(declare-fun a_7_34 () U)
(declare-fun a_7_35 () U)
(declare-fun a_7_36 () U)
(declare-fun a_7_37 () U)
(declare-fun a_7_38 () U)
(declare-fun a_7_39 () U)
(declare-fun a_8_0 () U)
(declare-fun a_8_1 () U)
(declare-fun a_8_2 () U)
(declare-fun a_8_3 () U)
(declare-fun a_8_4 () U)
(declare-fun a_8_5 () U)
(declare-fun a_8_6 () U)
(declare-fun a_8_7 () U)
(declare-fun a_8_8 () U)
(declare-fun a_8_9 () U)
(declare-fun a_8_10 () U)
(declare-fun a_8_11 () U)
(declare-fun a_8_12 () U)
(declare-fun a_8_13 () U)
(declare-fun a_8_14 () U)
(declare-fun a_8_15 () U)
(declare-fun a_8_16 () U)
(declare-fun a_8_17 () U)
(declare-fun a_8_18 () U)
(declare-fun a_8_19 () U)
(declare-fun a_8_20 () U)
(declare-fun a_8_21 () U)
(declare-fun a_8_22 () U)
(declare-fun a_8_23 () U)
(declare-fun a_8_24 () U)
(declare-fun a_8_25 () U)
(declare-fun a_8_26 () U)
(declare-fun a_8_27 () U)
(declare-fun a_8_28 () U)
(declare-fun a_8_29 () U)
(declare-fun a_8_30 () U)
(declare-fun a_8_31 () U)
(declare-fun a_8_32 () U)
(declare-fun a_8_33 () U)
(declare-fun a_8_34 () U)
(declare-fun a_8_35 () U)
(declare-fun a_8_36 () U)
(declare-fun a_8_37 () U)
(declare-fun a_8_38 () U)
(declare-fun a_8_39 () U)
(declare-fun a_9_0 () U)
(declare-fun a_9_1 () U)
(declare-fun a_9_2 () U)
(declare-fun a_9_3 () U)
(declare-fun a_9_4 () U)
(declare-fun a_9_5 () U)
(declare-fun a_9_6 () U)
(declare-fun a_9_7 () U)
(declare-fun a_9_8 () U)
(declare-fun a_9_9 () U)
(declare-fun a_9_10 () U)
(declare-fun a_9_11 () U)
(declare-fun a_9_12 () U)
(declare-fun a_9_13 () U)
(declare-fun a_9_14 () U)
(declare-fun a_9_15 () U)
(declare-fun a_9_16 () U)
(declare-fun a_9_17 () U)
(declare-fun a_9_18 () U)
(declare-fun a_9_19 () U)
(declare-fun a_9_20 () U)
(declare-fun a_9_21 () U)
(declare-fun a_9_22 () U)
(declare-fun a_9_23 () U)
(declare-fun a_9_24 () U)
(declare-fun a_9_25 () U)
(declare-fun a_9_26 () U)
(declare-fun a_9_27 () U)
(declare-fun a_9_28 () U)
(declare-fun a_9_29 () U)
(declare-fun a_9_30 () U)
(declare-fun a_9_31 () U)
(declare-fun a_9_32 () U)
(declare-fun a_9_33 () U)
(declare-fun a_9_34 () U)
(declare-fun a_9_35 () U)
(declare-fun a_9_36 () U)
(declare-fun a_9_37 () U)
(declare-fun a_9_38 () U)
(declare-fun a_9_39 () U)
(declare-fun a_10_0 () U)
(declare-fun a_10_1 () U)
(declare-fun a_10_2 () U)
(declare-fun a_10_3 () U)
(declare-fun a_10_4 () U)
(declare-fun a_10_5 () U)
(declare-fun a_10_6 () U)
(declare-fun a_10_7 () U)
(declare-fun a_10_8 () U)
(declare-fun a_10_9 () U)
(declare-fun a_10_10 () U)
(declare-fun a_10_11 () U)
(declare-fun a_10_12 () U)
(declare-fun a_10_13 () U)
(declare-fun a_10_14 () U)
(declare-fun a_10_15 () U)
(declare-fun a_10_16 () U)
(declare-fun a_10_17 () U)
(declare-fun a_10_18 () U)
(declare-fun a_10_19 () U)
(declare-fun a_10_20 () U)
(declare-fun a_10_21 () U)
(declare-fun a_10_22 () U)
(declare-fun a_10_23 () U)
(declare-fun a_10_24 () U)
(declare-fun a_10_25 () U)
(declare-fun a_10_26 () U)
(declare-fun a_10_27 () U)
(declare-fun a_10_28 () U)
(declare-fun a_10_29 () U)
(declare-fun a_10_30 () U)
(declare-fun a_10_31 () U)
(declare-fun a_10_32 () U)
(declare-fun a_10_33 () U)
(declare-fun a_10_34 () U)
(declare-fun a_10_35 () U)
(declare-fun a_10_36 () U)
(declare-fun a_10_37 () U)
(declare-fun a_10_38 () U)
(declare-fun a_10_39 () U)
(declare-fun a_11_0 () U)
(declare-fun a_11_1 () U)
(declare-fun a_11_2 () U)
(declare-fun a_11_3 () U)
(declare-fun a_11_4 () U)
(declare-fun a_11_5 () U)
(declare-fun a_11_6 () U)
(declare-fun a_11_7 () U)
(declare-fun a_11_8 () U)
(declare-fun a_11_9 () U)
(declare-fun a_11_10 () U)
(declare-fun a_11_11 () U)
(declare-fun a_11_12 () U)
(declare-fun a_11_13 () U)
(declare-fun a_11_14 () U)
(declare-fun a_11_15 () U)
(declare-fun a_11_16 () U)
(declare-fun a_11_17 () U)
(declare-fun a_11_18 () U)
(declare-fun a_11_19 () U)
(declare-fun a_11_20 () U)
(declare-fun a_11_21 () U)
(declare-fun a_11_22 () U)
(declare-fun a_11_23 () U)
(declare-fun a_11_24 () U)
(declare-fun a_11_25 () U)
(declare-fun a_11_26 () U)
(declare-fun a_11_27 () U)
(declare-fun a_11_28 () U)
(declare-fun a_11_29 () U)
(declare-fun a_11_30 () U)
(declare-fun a_11_31 () U)
(declare-fun a_11_32 () U)
(declare-fun a_11_33 () U)
(declare-fun a_11_34 () U)
(declare-fun a_11_35 () U)
(declare-fun a_11_36 () U)
(declare-fun a_11_37 () U)
(declare-fun a_11_38 () U)
(declare-fun a_11_39 () U)
(declare-fun a_12_0 () U)
(declare-fun a_12_1 () U)
(declare-fun a_12_2 () U)
(declare-fun a_12_3 () U)
(declare-fun a_12_4 () U)
(declare-fun a_12_5 () U)
(declare-fun a_12_6 () U)
(declare-fun a_12_7 () U)
(declare-fun a_12_8 () U)
(declare-fun a_12_9 () U)
(declare-fun a_12_10 () U)
(declare-fun a_12_11 () U)
(declare-fun a_12_12 () U)
(declare-fun a_12_13 () U)
(declare-fun a_12_14 () U)
(declare-fun a_12_15 () U)
(declare-fun a_12_16 () U)
(declare-fun a_12_17 () U)
(declare-fun a_12_18 () U)
(declare-fun a_12_19 () U)
(declare-fun a_12_20 () U)
(declare-fun a_12_21 () U)
(declare-fun a_12_22 () U)
(declare-fun a_12_23 () U)
(declare-fun a_12_24 () U)
(declare-fun a_12_25 () U)
(declare-fun a_12_26 () U)
(declare-fun a_12_27 () U)
(declare-fun a_12_28 () U)
(declare-fun a_12_29 () U)
(declare-fun a_12_30 () U)
(declare-fun a_12_31 () U)
(declare-fun a_12_32 () U)
(declare-fun a_12_33 () U)
(declare-fun a_12_34 () U)
(declare-fun a_12_35 () U)
(declare-fun a_12_36 () U)
(declare-fun a_12_37 () U)
(declare-fun a_12_38 () U)
(declare-fun a_12_39 () U)
(declare-fun a_13_0 () U)
(declare-fun a_13_1 () U)
(declare-fun a_13_2 () U)
(declare-fun a_13_3 () U)
(declare-fun a_13_4 () U)
(declare-fun a_13_5 () U)
(declare-fun a_13_6 () U)
(declare-fun a_13_7 () U)
(declare-fun a_13_8 () U)
(declare-fun a_13_9 () U)
(declare-fun a_13_10 () U)
(declare-fun a_13_11 () U)
(declare-fun a_13_12 () U)
(declare-fun a_13_13 () U)
(declare-fun a_13_14 () U)
(declare-fun a_13_15 () U)
(declare-fun a_13_16 () U)
(declare-fun a_13_17 () U)
(declare-fun a_13_18 () U)
(declare-fun a_13_19 () U)
(declare-fun a_13_20 () U)
(declare-fun a_13_21 () U)
(declare-fun a_13_22 () U)
(declare-fun a_13_23 () U)
(declare-fun a_13_24 () U)
(declare-fun a_13_25 () U)
(declare-fun a_13_26 () U)
(declare-fun a_13_27 () U)
(declare-fun a_13_28 () U)
(declare-fun a_13_29 () U)
(declare-fun a_13_30 () U)
(declare-fun a_13_31 () U)
(declare-fun a_13_32 () U)
(declare-fun a_13_33 () U)
(declare-fun a_13_34 () U)
(declare-fun a_13_35 () U)
(declare-fun a_13_36 () U)
(declare-fun a_13_37 () U)
(declare-fun a_13_38 () U)
(declare-fun a_13_39 () U)
(declare-fun a_14_0 () U)
(declare-fun a_14_1 () U)
(declare-fun a_14_2 () U)
(declare-fun a_14_3 () U)
(declare-fun a_14_4 () U)
(declare-fun a_14_5 () U)
(declare-fun a_14_6 () U)
(declare-fun a_14_7 () U)
(declare-fun a_14_8 () U)
(declare-fun a_14_9 () U)
(declare-fun a_14_10 () U)
(declare-fun a_14_11 () U)
(declare-fun a_14_12 () U)
(declare-fun a_14_13 () U)
(declare-fun a_14_14 () U)
(declare-fun a_14_15 () U)
(declare-fun a_14_16 () U)
(declare-fun a_14_17 () U)
(declare-fun a_14_18 () U)
(declare-fun a_14_19 () U)
(declare-fun a_14_20 () U)
(declare-fun a_14_21 () U)
(declare-fun a_14_22 () U)
(declare-fun a_14_23 () U)
(declare-fun a_14_24 () U)
(declare-fun a_14_25 () U)
(declare-fun a_14_26 () U)
(declare-fun a_14_27 () U)
(declare-fun a_14_28 () U)
(declare-fun a_14_29 () U)
(declare-fun a_14_30 () U)
(declare-fun a_14_31 () U)
(declare-fun a_14_32 () U)
(declare-fun a_14_33 () U)
(declare-fun a_14_34 () U)
(declare-fun a_14_35 () U)
(declare-fun a_14_36 () U)
(declare-fun a_14_37 () U)
(declare-fun a_14_38 () U)
(declare-fun a_14_39 () U)
(declare-fun a_15_0 () U)
(declare-fun a_15_1 () U)
(declare-fun a_15_2 () U)
(declare-fun a_15_3 () U)
(declare-fun a_15_4 () U)
(declare-fun a_15_5 () U)
(declare-fun a_15_6 () U)
(declare-fun a_15_7 () U)
(declare-fun a_15_8 () U)
(declare-fun a_15_9 () U)
(declare-fun a_15_10 () U)
(declare-fun a_15_11 () U)
(declare-fun a_15_12 () U)
(declare-fun a_15_13 () U)
(declare-fun a_15_14 () U)
(declare-fun a_15_15 () U)
(declare-fun a_15_16 () U)
(declare-fun a_15_17 () U)
(declare-fun a_15_18 () U)
(declare-fun a_15_19 () U)
(declare-fun a_15_20 () U)
(declare-fun a_15_21 () U)
(declare-fun a_15_22 () U)
(declare-fun a_15_23 () U)
(declare-fun a_15_24 () U)
(declare-fun a_15_25 () U)
(declare-fun a_15_26 () U)
(declare-fun a_15_27 () U)
(declare-fun a_15_28 () U)
(declare-fun a_15_29 () U)
(declare-fun a_15_30 () U)
(declare-fun a_15_31 () U)
(declare-fun a_15_32 () U)
(declare-fun a_15_33 () U)
(declare-fun a_15_34 () U)
(declare-fun a_15_35 () U)
(declare-fun a_15_36 () U)
(declare-fun a_15_37 () U)
(declare-fun a_15_38 () U)
(declare-fun a_15_39 () U)
(declare-fun a_16_0 () U)
(declare-fun a_16_1 () U)
(declare-fun a_16_2 () U)
(declare-fun a_16_3 () U)
(declare-fun a_16_4 () U)
(declare-fun a_16_5 () U)
(declare-fun a_16_6 () U)
(declare-fun a_16_7 () U)
(declare-fun a_16_8 () U)
(declare-fun a_16_9 () U)
(declare-fun a_16_10 () U)
(declare-fun a_16_11 () U)
(declare-fun a_16_12 () U)
(declare-fun a_16_13 () U)
(declare-fun a_16_14 () U)
(declare-fun a_16_15 () U)
(declare-fun a_16_16 () U)
(declare-fun a_16_17 () U)
(declare-fun a_16_18 () U)
(declare-fun a_16_19 () U)
(declare-fun a_16_20 () U)
(declare-fun a_16_21 () U)
(declare-fun a_16_22 () U)
(declare-fun a_16_23 () U)
(declare-fun a_16_24 () U)
(declare-fun a_16_25 () U)
(declare-fun a_16_26 () U)
(declare-fun a_16_27 () U)
(declare-fun a_16_28 () U)
(declare-fun a_16_29 () U)
(declare-fun a_16_30 () U)
(declare-fun a_16_31 () U)
(declare-fun a_16_32 () U)
(declare-fun a_16_33 () U)
(declare-fun a_16_34 () U)
(declare-fun a_16_35 () U)
(declare-fun a_16_36 () U)
(declare-fun a_16_37 () U)
(declare-fun a_16_38 () U)
(declare-fun a_16_39 () U)
(declare-fun a_17_0 () U)
(declare-fun a_17_1 () U)
(declare-fun a_17_2 () U)
(declare-fun a_17_3 () U)
(declare-fun a_17_4 () U)
(declare-fun a_17_5 () U)
(declare-fun a_17_6 () U)
(declare-fun a_17_7 () U)
(declare-fun a_17_8 () U)
(declare-fun a_17_9 () U)
(declare-fun a_17_10 () U)
(declare-fun a_17_11 () U)
(declare-fun a_17_12 () U)
(declare-fun a_17_13 () U)
(declare-fun a_17_14 () U)
(declare-fun a_17_15 () U)
(declare-fun a_17_16 () U)
(declare-fun a_17_17 () U)
(declare-fun a_17_18 () U)
(declare-fun a_17_19 () U)
(declare-fun a_17_20 () U)
(declare-fun a_17_21 () U)
(declare-fun a_17_22 () U)
(declare-fun a_17_23 () U)
(declare-fun a_17_24 () U)
(declare-fun a_17_25 () U)
(declare-fun a_17_26 () U)
(declare-fun a_17_27 () U)
(declare-fun a_17_28 () U)
(declare-fun a_17_29 () U)
(declare-fun a_17_30 () U)
(declare-fun a_17_31 () U)
(declare-fun a_17_32 () U)
(declare-fun a_17_33 () U)
(declare-fun a_17_34 () U)
(declare-fun a_17_35 () U)
(declare-fun a_17_36 () U)
(declare-fun a_17_37 () U)
(declare-fun a_17_38 () U)
(declare-fun a_17_39 () U)
(declare-fun a_18_0 () U)
(declare-fun a_18_1 () U)
(declare-fun a_18_2 () U)
(declare-fun a_18_3 () U)
(declare-fun a_18_4 () U)
(declare-fun a_18_5 () U)
(declare-fun a_18_6 () U)
(declare-fun a_18_7 () U)
(declare-fun a_18_8 () U)
(declare-fun a_18_9 () U)
(declare-fun a_18_10 () U)
(declare-fun a_18_11 () U)
(declare-fun a_18_12 () U)
(declare-fun a_18_13 () U)
(declare-fun a_18_14 () U)
(declare-fun a_18_15 () U)
(declare-fun a_18_16 () U)
(declare-fun a_18_17 () U)
(declare-fun a_18_18 () U)
(declare-fun a_18_19 () U)
(declare-fun a_18_20 () U)
(declare-fun a_18_21 () U)
(declare-fun a_18_22 () U)
(declare-fun a_18_23 () U)
(declare-fun a_18_24 () U)
(declare-fun a_18_25 () U)
(declare-fun a_18_26 () U)
(declare-fun a_18_27 () U)
(declare-fun a_18_28 () U)
(declare-fun a_18_29 () U)
(declare-fun a_18_30 () U)
(declare-fun a_18_31 () U)
(declare-fun a_18_32 () U)
(declare-fun a_18_33 () U)
(declare-fun a_18_34 () U)
(declare-fun a_18_35 () U)
(declare-fun a_18_36 () U)
(declare-fun a_18_37 () U)
(declare-fun a_18_38 () U)
(declare-fun a_18_39 () U)
(declare-fun a_19_0 () U)
(declare-fun a_19_1 () U)
(declare-fun a_19_2 () U)
(declare-fun a_19_3 () U)
(declare-fun a_19_4 () U)
(declare-fun a_19_5 () U)
(declare-fun a_19_6 () U)
(declare-fun a_19_7 () U)
(declare-fun a_19_8 () U)
(declare-fun a_19_9 () U)
(declare-fun a_19_10 () U)
(declare-fun a_19_11 () U)
(declare-fun a_19_12 () U)
(declare-fun a_19_13 () U)
(declare-fun a_19_14 () U)
(declare-fun a_19_15 () U)
(declare-fun a_19_16 () U)
(declare-fun a_19_17 () U)
(declare-fun a_19_18 () U)
(declare-fun a_19_19 () U)
(declare-fun a_19_20 () U)
(declare-fun a_19_21 () U)
(declare-fun a_19_22 () U)
(declare-fun a_19_23 () U)
(declare-fun a_19_24 () U)
(declare-fun a_19_25 () U)
(declare-fun a_19_26 () U)
(declare-fun a_19_27 () U)
(declare-fun a_19_28 () U)
(declare-fun a_19_29 () U)
(declare-fun a_19_30 () U)
(declare-fun a_19_31 () U)
(declare-fun a_19_32 () U)
(declare-fun a_19_33 () U)
(declare-fun a_19_34 () U)
(declare-fun a_19_35 () U)
(declare-fun a_19_36 () U)
(declare-fun a_19_37 () U)
(declare-fun a_19_38 () U)
(declare-fun a_19_39 () U)
(declare-fun a_20_0 () U)
(declare-fun a_20_1 () U)
(declare-fun a_20_2 () U)
(declare-fun a_20_3 () U)
(declare-fun a_20_4 () U)
(declare-fun a_20_5 () U)
(declare-fun a_20_6 () U)
(declare-fun a_20_7 () U)
(declare-fun a_20_8 () U)
(declare-fun a_20_9 () U)
(declare-fun a_20_10 () U)
(declare-fun a_20_11 () U)
(declare-fun a_20_12 () U)
(declare-fun a_20_13 () U)
(declare-fun a_20_14 () U)
(declare-fun a_20_15 () U)
(declare-fun a_20_16 () U)
(declare-fun a_20_17 () U)
(declare-fun a_20_18 () U)
(declare-fun a_20_19 () U)
(declare-fun a_20_20 () U)
(declare-fun a_20_21 () U)
(declare-fun a_20_22 () U)
(declare-fun a_20_23 () U)
(declare-fun a_20_24 () U)
(declare-fun a_20_25 () U)
(declare-fun a_20_26 () U)
(declare-fun a_20_27 () U)
(declare-fun a_20_28 () U)
(declare-fun a_20_29 () U)
(declare-fun a_20_30 () U)
(declare-fun a_20_31 () U)
(declare-fun a_20_32 () U)
(declare-fun a_20_33 () U)
(declare-fun a_20_34 () U)
(declare-fun a_20_35 () U)
(declare-fun a_20_36 () U)
(declare-fun a_20_37 () U)
(declare-fun a_20_38 () U)
(declare-fun a_20_39 () U)
(declare-fun a_21_0 () U)
(declare-fun a_21_1 () U)
(declare-fun a_21_2 () U)
(declare-fun a_21_3 () U)
(declare-fun a_21_4 () U)
(declare-fun a_21_5 () U)
(declare-fun a_21_6 () U)
(declare-fun a_21_7 () U)
(declare-fun a_21_8 () U)
(declare-fun a_21_9 () U)
(declare-fun a_21_10 () U)
(declare-fun a_21_11 () U)
(declare-fun a_21_12 () U)
(declare-fun a_21_13 () U)
(declare-fun a_21_14 () U)
(declare-fun a_21_15 () U)
(declare-fun a_21_16 () U)
(declare-fun a_21_17 () U)
(declare-fun a_21_18 () U)
(declare-fun a_21_19 () U)
(declare-fun a_21_20 () U)
(declare-fun a_21_21 () U)
(declare-fun a_21_22 () U)
(declare-fun a_21_23 () U)
(declare-fun a_21_24 () U)
(declare-fun a_21_25 () U)
(declare-fun a_21_26 () U)
(declare-fun a_21_27 () U)
(declare-fun a_21_28 () U)
(declare-fun a_21_29 () U)
(declare-fun a_21_30 () U)
(declare-fun a_21_31 () U)
(declare-fun a_21_32 () U)
(declare-fun a_21_33 () U)
(declare-fun a_21_34 () U)
(declare-fun a_21_35 () U)
(declare-fun a_21_36 () U)
(declare-fun a_21_37 () U)
(declare-fun a_21_38 () U)
(declare-fun a_21_39 () U)
(declare-fun a_22_0 () U)
(declare-fun a_22_1 () U)
(declare-fun a_22_2 () U)
(declare-fun a_22_3 () U)
(declare-fun a_22_4 () U)
(declare-fun a_22_5 () U)
(declare-fun a_22_6 () U)
(declare-fun a_22_7 () U)
(declare-fun a_22_8 () U)
(declare-fun a_22_9 () U)
(declare-fun a_22_10 () U)
(declare-fun a_22_11 () U)
(declare-fun a_22_12 () U)
(declare-fun a_22_13 () U)
(declare-fun a_22_14 () U)
(declare-fun a_22_15 () U)
(declare-fun a_22_16 () U)
(declare-fun a_22_17 () U)
(declare-fun a_22_18 () U)
(declare-fun a_22_19 () U)
(declare-fun a_22_20 () U)
(declare-fun a_22_21 () U)
(declare-fun a_22_22 () U)
(declare-fun a_22_23 () U)
(declare-fun a_22_24 () U)
(declare-fun a_22_25 () U)
(declare-fun a_22_26 () U)
(declare-fun a_22_27 () U)
(declare-fun a_22_28 () U)
(declare-fun a_22_29 () U)
(declare-fun a_22_30 () U)
(declare-fun a_22_31 () U)
(declare-fun a_22_32 () U)
(declare-fun a_22_33 () U)
(declare-fun a_22_34 () U)
(declare-fun a_22_35 () U)
(declare-fun a_22_36 () U)
(declare-fun a_22_37 () U)
(declare-fun a_22_38 () U)
(declare-fun a_22_39 () U)
(declare-fun a_23_0 () U)
(declare-fun a_23_1 () U)
(declare-fun a_23_2 () U)
(declare-fun a_23_3 () U)
(declare-fun a_23_4 () U)
(declare-fun a_23_5 () U)
(declare-fun a_23_6 () U)
(declare-fun a_23_7 () U)
(declare-fun a_23_8 () U)
(declare-fun a_23_9 () U)
(declare-fun a_23_10 () U)
(declare-fun a_23_11 () U)
(declare-fun a_23_12 () U)
(declare-fun a_23_13 () U)
(declare-fun a_23_14 () U)
(declare-fun a_23_15 () U)
(declare-fun a_23_16 () U)
(declare-fun a_23_17 () U)
(declare-fun a_23_18 () U)
(declare-fun a_23_19 () U)
(declare-fun a_23_20 () U)
(declare-fun a_23_21 () U)
(declare-fun a_23_22 () U)
(declare-fun a_23_23 () U)
(declare-fun a_23_24 () U)
(declare-fun a_23_25 () U)
(declare-fun a_23_26 () U)
(declare-fun a_23_27 () U)
(declare-fun a_23_28 () U)
(declare-fun a_23_29 () U)
(declare-fun a_23_30 () U)
(declare-fun a_23_31 () U)
(declare-fun a_23_32 () U)
(declare-fun a_23_33 () U)
(declare-fun a_23_34 () U)
(declare-fun a_23_35 () U)
(declare-fun a_23_36 () U)
(declare-fun a_23_37 () U)
(declare-fun a_23_38 () U)
(declare-fun a_23_39 () U)
(declare-fun a_24_0 () U)
(declare-fun a_24_1 () U)
(declare-fun a_24_2 () U)
(declare-fun a_24_3 () U)
(declare-fun a_24_4 () U)
(declare-fun a_24_5 () U)
(declare-fun a_24_6 () U)
(declare-fun a_24_7 () U)
(declare-fun a_24_8 () U)
(declare-fun a_24_9 () U)
(declare-fun a_24_10 () U)
(declare-fun a_24_11 () U)
(declare-fun a_24_12 () U)
(declare-fun a_24_13 () U)
(declare-fun a_24_14 () U)
(declare-fun a_24_15 () U)
(declare-fun a_24_16 () U)
(declare-fun a_24_17 () U)
(declare-fun a_24_18 () U)
(declare-fun a_24_19 () U)
(declare-fun a_24_20 () U)
(declare-fun a_24_21 () U)
(declare-fun a_24_22 () U)
(declare-fun a_24_23 () U)
(declare-fun a_24_24 () U)
(declare-fun a_24_25 () U)
(declare-fun a_24_26 () U)
(declare-fun a_24_27 () U)
(declare-fun a_24_28 () U)
(declare-fun a_24_29 () U)
(declare-fun a_24_30 () U)
(declare-fun a_24_31 () U)
(declare-fun a_24_32 () U)
(declare-fun a_24_33 () U)
(declare-fun a_24_34 () U)
(declare-fun a_24_35 () U)
(declare-fun a_24_36 () U)
(declare-fun a_24_37 () U)
(declare-fun a_24_38 () U)
(declare-fun a_24_39 () U)
(declare-fun a_25_0 () U)
(declare-fun a_25_1 () U)
(declare-fun a_25_2 () U)
(declare-fun a_25_3 () U)
(declare-fun a_25_4 () U)
(declare-fun a_25_5 () U)
(declare-fun a_25_6 () U)
(declare-fun a_25_7 () U)
(declare-fun a_25_8 () U)
(declare-fun a_25_9 () U)
(declare-fun a_25_10 () U)
(declare-fun a_25_11 () U)
(declare-fun a_25_12 () U)
(declare-fun a_25_13 () U)
(declare-fun a_25_14 () U)
(declare-fun a_25_15 () U)
(declare-fun a_25_16 () U)
(declare-fun a_25_17 () U)
(declare-fun a_25_18 () U)
(declare-fun a_25_19 () U)
(declare-fun a_25_20 () U)
(declare-fun a_25_21 () U)
(declare-fun a_25_22 () U)
(declare-fun a_25_23 () U)
(declare-fun a_25_24 () U)
(declare-fun a_25_25 () U)
(declare-fun a_25_26 () U)
(declare-fun a_25_27 () U)
(declare-fun a_25_28 () U)
(declare-fun a_25_29 () U)
(declare-fun a_25_30 () U)
(declare-fun a_25_31 () U)
(declare-fun a_25_32 () U)
(declare-fun a_25_33 () U)
(declare-fun a_25_34 () U)
(declare-fun a_25_35 () U)
(declare-fun a_25_36 () U)
(declare-fun a_25_37 () U)
(declare-fun a_25_38 () U)
(declare-fun a_25_39 () U)
(declare-fun a_26_0 () U)
(declare-fun a_26_1 () U)
(declare-fun a_26_2 () U)
(declare-fun a_26_3 () U)
(declare-fun a_26_4 () U)
(declare-fun a_26_5 () U)
(declare-fun a_26_6 () U)
(declare-fun a_26_7 () U)
(declare-fun a_26_8 () U)
(declare-fun a_26_9 () U)
(declare-fun a_26_10 () U)
(declare-fun a_26_11 () U)
(declare-fun a_26_12 () U)
(declare-fun a_26_13 () U)
(declare-fun a_26_14 () U)
(declare-fun a_26_15 () U)
(declare-fun a_26_16 () U)
(declare-fun a_26_17 () U)
(declare-fun a_26_18 () U)
(declare-fun a_26_19 () U)
(declare-fun a_26_20 () U)
(declare-fun a_26_21 () U)
(declare-fun a_26_22 () U)
(declare-fun a_26_23 () U)
(declare-fun a_26_24 () U)
(declare-fun a_26_25 () U)
(declare-fun a_26_26 () U)
(declare-fun a_26_27 () U)
(declare-fun a_26_28 () U)
(declare-fun a_26_29 () U)
(declare-fun a_26_30 () U)
(declare-fun a_26_31 () U)
(declare-fun a_26_32 () U)
(declare-fun a_26_33 () U)
(declare-fun a_26_34 () U)
(declare-fun a_26_35 () U)
(declare-fun a_26_36 () U)
(declare-fun a_26_37 () U)
(declare-fun a_26_38 () U)
(declare-fun a_26_39 () U)
(declare-fun a_27_0 () U)
(declare-fun a_27_1 () U)
(declare-fun a_27_2 () U)
(declare-fun a_27_3 () U)
(declare-fun a_27_4 () U)
(declare-fun a_27_5 () U)
(declare-fun a_27_6 () U)
(declare-fun a_27_7 () U)
(declare-fun a_27_8 () U)
(declare-fun a_27_9 () U)
(declare-fun a_27_10 () U)
(declare-fun a_27_11 () U)
(declare-fun a_27_12 () U)
(declare-fun a_27_13 () U)
(declare-fun a_27_14 () U)
(declare-fun a_27_15 () U)
(declare-fun a_27_16 () U)
(declare-fun a_27_17 () U)
(declare-fun a_27_18 () U)
(declare-fun a_27_19 () U)
(declare-fun a_27_20 () U)
(declare-fun a_27_21 () U)
(declare-fun a_27_22 () U)
(declare-fun a_27_23 () U)
(declare-fun a_27_24 () U)
(declare-fun a_27_25 () U)
(declare-fun a_27_26 () U)
(declare-fun a_27_27 () U)
(declare-fun a_27_28 () U)
(declare-fun a_27_29 () U)
(declare-fun a_27_30 () U)
(declare-fun a_27_31 () U)
(declare-fun a_27_32 () U)
(declare-fun a_27_33 () U)
(declare-fun a_27_34 () U)
(declare-fun a_27_35 () U)
(declare-fun a_27_36 () U)
(declare-fun a_27_37 () U)
(declare-fun a_27_38 () U)
(declare-fun a_27_39 () U)
(declare-fun a_28_0 () U)
(declare-fun a_28_1 () U)
(declare-fun a_28_2 () U)
(declare-fun a_28_3 () U)
(declare-fun a_28_4 () U)
(declare-fun a_28_5 () U)
(declare-fun a_28_6 () U)
(declare-fun a_28_7 () U)
(declare-fun a_28_8 () U)
(declare-fun a_28_9 () U)
(declare-fun a_28_10 () U)
(declare-fun a_28_11 () U)
(declare-fun a_28_12 () U)
(declare-fun a_28_13 () U)
(declare-fun a_28_14 () U)
(declare-fun a_28_15 () U)
(declare-fun a_28_16 () U)
(declare-fun a_28_17 () U)
(declare-fun a_28_18 () U)
(declare-fun a_28_19 () U)
(declare-fun a_28_20 () U)
(declare-fun a_28_21 () U)
(declare-fun a_28_22 () U)
(declare-fun a_28_23 () U)
(declare-fun a_28_24 () U)
(declare-fun a_28_25 () U)
(declare-fun a_28_26 () U)
(declare-fun a_28_27 () U)
(declare-fun a_28_28 () U)
(declare-fun a_28_29 () U)
(declare-fun a_28_30 () U)
(declare-fun a_28_31 () U)
(declare-fun a_28_32 () U)
(declare-fun a_28_33 () U)
(declare-fun a_28_34 () U)
(declare-fun a_28_35 () U)
(declare-fun a_28_36 () U)
(declare-fun a_28_37 () U)
(declare-fun a_28_38 () U)
(declare-fun a_28_39 () U)
(declare-fun a_29_0 () U)
(declare-fun a_29_1 () U)
(declare-fun a_29_2 () U)
(declare-fun a_29_3 () U)
(declare-fun a_29_4 () U)
(declare-fun a_29_5 () U)
(declare-fun a_29_6 () U)
(declare-fun a_29_7 () U)
(declare-fun a_29_8 () U)
(declare-fun a_29_9 () U)
(declare-fun a_29_10 () U)
(declare-fun a_29_11 () U)
(declare-fun a_29_12 () U)
(declare-fun a_29_13 () U)
(declare-fun a_29_14 () U)
(declare-fun a_29_15 () U)
(declare-fun a_29_16 () U)
(declare-fun a_29_17 () U)
(declare-fun a_29_18 () U)
(declare-fun a_29_19 () U)
(declare-fun a_29_20 () U)
(declare-fun a_29_21 () U)
(declare-fun a_29_22 () U)
(declare-fun a_29_23 () U)
(declare-fun a_29_24 () U)
(declare-fun a_29_25 () U)
(declare-fun a_29_26 () U)
(declare-fun a_29_27 () U)
(declare-fun a_29_28 () U)
(declare-fun a_29_29 () U)
(declare-fun a_29_30 () U)
(declare-fun a_29_31 () U)
(declare-fun a_29_32 () U)
(declare-fun a_29_33 () U)
(declare-fun a_29_34 () U)
(declare-fun a_29_35 () U)
(declare-fun a_29_36 () U)
(declare-fun a_29_37 () U)
(declare-fun a_29_38 () U)
(declare-fun a_29_39 () U)
(declare-fun a_30_0 () U)
(declare-fun a_30_1 () U)
(declare-fun a_30_2 () U)
(declare-fun a_30_3 () U)
(declare-fun a_30_4 () U)
(declare-fun a_30_5 () U)
(declare-fun a_30_6 () U)
(declare-fun a_30_7 () U)
(declare-fun a_30_8 () U)
(declare-fun a_30_9 () U)
(declare-fun a_30_10 () U)
(declare-fun a_30_11 () U)
(declare-fun a_30_12 () U)
(declare-fun a_30_13 () U)
(declare-fun a_30_14 () U)
(declare-fun a_30_15 () U)
(declare-fun a_30_16 () U)
(declare-fun a_30_17 () U)
(declare-fun a_30_18 () U)
(declare-fun a_30_19 () U)
(declare-fun a_30_20 () U)
(declare-fun a_30_21 () U)
(declare-fun a_30_22 () U)
(declare-fun a_30_23 () U)
(declare-fun a_30_24 () U)
(declare-fun a_30_25 () U)
(declare-fun a_30_26 () U)
(declare-fun a_30_27 () U)
(declare-fun a_30_28 () U)
(declare-fun a_30_29 () U)
(declare-fun a_30_30 () U)
(declare-fun a_30_31 () U)
(declare-fun a_30_32 () U)
(declare-fun a_30_33 () U)
(declare-fun a_30_34 () U)
(declare-fun a_30_35 () U)
(declare-fun a_30_36 () U)
(declare-fun a_30_37 () U)
(declare-fun a_30_38 () U)
(declare-fun a_30_39 () U)
(declare-fun a_31_0 () U)
(declare-fun a_31_1 () U)
(declare-fun a_31_2 () U)
(declare-fun a_31_3 () U)
(declare-fun a_31_4 () U)
(declare-fun a_31_5 () U)
(declare-fun a_31_6 () U)
(declare-fun a_31_7 () U)
(declare-fun a_31_8 () U)
(declare-fun a_31_9 () U)
(declare-fun a_31_10 () U)
(declare-fun a_31_11 () U)
(declare-fun a_31_12 () U)
(declare-fun a_31_13 () U)
(declare-fun a_31_14 () U)
(declare-fun a_31_15 () U)
(declare-fun a_31_16 () U)
(declare-fun a_31_17 () U)
(declare-fun a_31_18 () U)
(declare-fun a_31_19 () U)
(declare-fun a_31_20 () U)
(declare-fun a_31_21 () U)
(declare-fun a_31_22 () U)
(declare-fun a_31_23 () U)
(declare-fun a_31_24 () U)
(declare-fun a_31_25 () U)
(declare-fun a_31_26 () U)
(declare-fun a_31_27 () U)
(declare-fun a_31_28 () U)
(declare-fun a_31_29 () U)
(declare-fun a_31_30 () U)
(declare-fun a_31_31 () U)
(declare-fun a_31_32 () U)
(declare-fun a_31_33 () U)
(declare-fun a_31_34 () U)
(declare-fun a_31_35 () U)
(declare-fun a_31_36 () U)
(declare-fun a_31_37 () U)
(declare-fun a_31_38 () U)
(declare-fun a_31_39 () U)
(declare-fun a_32_0 () U)
(declare-fun a_32_1 () U)
(declare-fun a_32_2 () U)
(declare-fun a_32_3 () U)
(declare-fun a_32_4 () U)
(declare-fun a_32_5 () U)
(declare-fun a_32_6 () U)
(declare-fun a_32_7 () U)
(declare-fun a_32_8 () U)
(declare-fun a_32_9 () U)
(declare-fun a_32_10 () U)
(declare-fun a_32_11 () U)
(declare-fun a_32_12 () U)
(declare-fun a_32_13 () U)
(declare-fun a_32_14 () U)
(declare-fun a_32_15 () U)
(declare-fun a_32_16 () U)
(declare-fun a_32_17 () U)
(declare-fun a_32_18 () U)
(declare-fun a_32_19 () U)
(declare-fun a_32_20 () U)
(declare-fun a_32_21 () U)
(declare-fun a_32_22 () U)
(declare-fun a_32_23 () U)
(declare-fun a_32_24 () U)
(declare-fun a_32_25 () U)
(declare-fun a_32_26 () U)
(declare-fun a_32_27 () U)
(declare-fun a_32_28 () U)
(declare-fun a_32_29 () U)
(declare-fun a_32_30 () U)
(declare-fun a_32_31 () U)
(declare-fun a_32_32 () U)
(declare-fun a_32_33 () U)
(declare-fun a_32_34 () U)
(declare-fun a_32_35 () U)
(declare-fun a_32_36 () U)
(declare-fun a_32_37 () U)
(declare-fun a_32_38 () U)
(declare-fun a_32_39 () U)
(declare-fun a_33_0 () U)
(declare-fun a_33_1 () U)
(declare-fun a_33_2 () U)
(declare-fun a_33_3 () U)
(declare-fun a_33_4 () U)
(declare-fun a_33_5 () U)
(declare-fun a_33_6 () U)
(declare-fun a_33_7 () U)
(declare-fun a_33_8 () U)
(declare-fun a_33_9 () U)
(declare-fun a_33_10 () U)
(declare-fun a_33_11 () U)
(declare-fun a_33_12 () U)
(declare-fun a_33_13 () U)
(declare-fun a_33_14 () U)
(declare-fun a_33_15 () U)
(declare-fun a_33_16 () U)
(declare-fun a_33_17 () U)
(declare-fun a_33_18 () U)
(declare-fun a_33_19 () U)
(declare-fun a_33_20 () U)
(declare-fun a_33_21 () U)
(declare-fun a_33_22 () U)
(declare-fun a_33_23 () U)
(declare-fun a_33_24 () U)
(declare-fun a_33_25 () U)
(declare-fun a_33_26 () U)
(declare-fun a_33_27 () U)
(declare-fun a_33_28 () U)
(declare-fun a_33_29 () U)
(declare-fun a_33_30 () U)
(declare-fun a_33_31 () U)
(declare-fun a_33_32 () U)
(declare-fun a_33_33 () U)
(declare-fun a_33_34 () U)
(declare-fun a_33_35 () U)
(declare-fun a_33_36 () U)
(declare-fun a_33_37 () U)
(declare-fun a_33_38 () U)
(declare-fun a_33_39 () U)
(declare-fun a_34_0 () U)
(declare-fun a_34_1 () U)
(declare-fun a_34_2 () U)
(declare-fun a_34_3 () U)
(declare-fun a_34_4 () U)
(declare-fun a_34_5 () U)
(declare-fun a_34_6 () U)
(declare-fun a_34_7 () U)
(declare-fun a_34_8 () U)
(declare-fun a_34_9 () U)
(declare-fun a_34_10 () U)
(declare-fun a_34_11 () U)
(declare-fun a_34_12 () U)
(declare-fun a_34_13 () U)
(declare-fun a_34_14 () U)
(declare-fun a_34_15 () U)
(declare-fun a_34_16 () U)
(declare-fun a_34_17 () U)
(declare-fun a_34_18 () U)
(declare-fun a_34_19 () U)
(declare-fun a_34_20 () U)
(declare-fun a_34_21 () U)
(declare-fun a_34_22 () U)
(declare-fun a_34_23 () U)
(declare-fun a_34_24 () U)
(declare-fun a_34_25 () U)
(declare-fun a_34_26 () U)
(declare-fun a_34_27 () U)
(declare-fun a_34_28 () U)
(declare-fun a_34_29 () U)
(declare-fun a_34_30 () U)
(declare-fun a_34_31 () U)
(declare-fun a_34_32 () U)
(declare-fun a_34_33 () U)
(declare-fun a_34_34 () U)
(declare-fun a_34_35 () U)
(declare-fun a_34_36 () U)
(declare-fun a_34_37 () U)
(declare-fun a_34_38 () U)
(declare-fun a_34_39 () U)
(declare-fun a_35_0 () U)
(declare-fun a_35_1 () U)
(declare-fun a_35_2 () U)
(declare-fun a_35_3 () U)
(declare-fun a_35_4 () U)
(declare-fun a_35_5 () U)
(declare-fun a_35_6 () U)
(declare-fun a_35_7 () U)
(declare-fun a_35_8 () U)
(declare-fun a_35_9 () U)
(declare-fun a_35_10 () U)
(declare-fun a_35_11 () U)
(declare-fun a_35_12 () U)
(declare-fun a_35_13 () U)
(declare-fun a_35_14 () U)
(declare-fun a_35_15 () U)
(declare-fun a_35_16 () U)
(declare-fun a_35_17 () U)
(declare-fun a_35_18 () U)
(declare-fun a_35_19 () U)
(declare-fun a_35_20 () U)
(declare-fun a_35_21 () U)
(declare-fun a_35_22 () U)
(declare-fun a_35_23 () U)
(declare-fun a_35_24 () U)
(declare-fun a_35_25 () U)
(declare-fun a_35_26 () U)
(declare-fun a_35_27 () U)
(declare-fun a_35_28 () U)
(declare-fun a_35_29 () U)
(declare-fun a_35_30 () U)
(declare-fun a_35_31 () U)
(declare-fun a_35_32 () U)
(declare-fun a_35_33 () U)
(declare-fun a_35_34 () U)
(declare-fun a_35_35 () U)
(declare-fun a_35_36 () U)
(declare-fun a_35_37 () U)
(declare-fun a_35_38 () U)
(declare-fun a_35_39 () U)
(declare-fun a_36_0 () U)
(declare-fun a_36_1 () U)
(declare-fun a_36_2 () U)
(declare-fun a_36_3 () U)
(declare-fun a_36_4 () U)
(declare-fun a_36_5 () U)
(declare-fun a_36_6 () U)
(declare-fun a_36_7 () U)
(declare-fun a_36_8 () U)
(declare-fun a_36_9 () U)
(declare-fun a_36_10 () U)
(declare-fun a_36_11 () U)
(declare-fun a_36_12 () U)
(declare-fun a_36_13 () U)
(declare-fun a_36_14 () U)
(declare-fun a_36_15 () U)
(declare-fun a_36_16 () U)
(declare-fun a_36_17 () U)
(declare-fun a_36_18 () U)
(declare-fun a_36_19 () U)
(declare-fun a_36_20 () U)
(declare-fun a_36_21 () U)
(declare-fun a_36_22 () U)
(declare-fun a_36_23 () U)
(declare-fun a_36_24 () U)
(declare-fun a_36_25 () U)
(declare-fun a_36_26 () U)
(declare-fun a_36_27 () U)
(declare-fun a_36_28 () U)
(declare-fun a_36_29 () U)
(declare-fun a_36_30 () U)
(declare-fun a_36_31 () U)
(declare-fun a_36_32 () U)
(declare-fun a_36_33 () U)
(declare-fun a_36_34 () U)
(declare-fun a_36_35 () U)
(declare-fun a_36_36 () U)
(declare-fun a_36_37 () U)
(declare-fun a_36_38 () U)
(declare-fun a_36_39 () U)
(declare-fun a_37_0 () U)
(declare-fun a_37_1 () U)
(declare-fun a_37_2 () U)
(declare-fun a_37_3 () U)
(declare-fun a_37_4 () U)
(declare-fun a_37_5 () U)
(declare-fun a_37_6 () U)
(declare-fun a_37_7 () U)
(declare-fun a_37_8 () U)
(declare-fun a_37_9 () U)
(declare-fun a_37_10 () U)
(declare-fun a_37_11 () U)
(declare-fun a_37_12 () U)
(declare-fun a_37_13 () U)
(declare-fun a_37_14 () U)
(declare-fun a_37_15 () U)
(declare-fun a_37_16 () U)
(declare-fun a_37_17 () U)
(declare-fun a_37_18 () U)
(declare-fun a_37_19 () U)
(declare-fun a_37_20 () U)
(declare-fun a_37_21 () U)
(declare-fun a_37_22 () U)
(declare-fun a_37_23 () U)
(declare-fun a_37_24 () U)
(declare-fun a_37_25 () U)
(declare-fun a_37_26 () U)
(declare-fun a_37_27 () U)
(declare-fun a_37_28 () U)
(declare-fun a_37_29 () U)
(declare-fun a_37_30 () U)
(declare-fun a_37_31 () U)
(declare-fun a_37_32 () U)
(declare-fun a_37_33 () U)
(declare-fun a_37_34 () U)
(declare-fun a_37_35 () U)
(declare-fun a_37_36 () U)
(declare-fun a_37_37 () U)
(declare-fun a_37_38 () U)
(declare-fun a_37_39 () U)
(declare-fun a_38_0 () U)
(declare-fun a_38_1 () U)
(declare-fun a_38_2 () U)
(declare-fun a_38_3 () U)
(declare-fun a_38_4 () U)
(declare-fun a_38_5 () U)
(declare-fun a_38_6 () U)
(declare-fun a_38_7 () U)
(declare-fun a_38_8 () U)
(declare-fun a_38_9 () U)
(declare-fun a_38_10 () U)
(declare-fun a_38_11 () U)
(declare-fun a_38_12 () U)
(declare-fun a_38_13 () U)
(declare-fun a_38_14 () U)
(declare-fun a_38_15 () U)
(declare-fun a_38_16 () U)
(declare-fun a_38_17 () U)
(declare-fun a_38_18 () U)
(declare-fun a_38_19 () U)
(declare-fun a_38_20 () U)
(declare-fun a_38_21 () U)
(declare-fun a_38_22 () U)
(declare-fun a_38_23 () U)
(declare-fun a_38_24 () U)
(declare-fun a_38_25 () U)
(declare-fun a_38_26 () U)
(declare-fun a_38_27 () U)
(declare-fun a_38_28 () U)
(declare-fun a_38_29 () U)
(declare-fun a_38_30 () U)
(declare-fun a_38_31 () U)
(declare-fun a_38_32 () U)
(declare-fun a_38_33 () U)
(declare-fun a_38_34 () U)
(declare-fun a_38_35 () U)
(declare-fun a_38_36 () U)
(declare-fun a_38_37 () U)
(declare-fun a_38_38 () U)
(declare-fun a_38_39 () U)
(declare-fun a_39_0 () U)
(declare-fun a_39_1 () U)
(declare-fun a_39_2 () U)
(declare-fun a_39_3 () U)
(declare-fun a_39_4 () U)
(declare-fun a_39_5 () U)
(declare-fun a_39_6 () U)
(declare-fun a_39_7 () U)
(declare-fun a_39_8 () U)
(declare-fun a_39_9 () U)
(declare-fun a_39_10 () U)
(declare-fun a_39_11 () U)
(declare-fun a_39_12 () U)
(declare-fun a_39_13 () U)
(declare-fun a_39_14 () U)
(declare-fun a_39_15 () U)
(declare-fun a_39_16 () U)
(declare-fun a_39_17 () U)
(declare-fun a_39_18 () U)
(declare-fun a_39_19 () U)
(declare-fun a_39_20 () U)
(declare-fun a_39_21 () U)
(declare-fun a_39_22 () U)
(declare-fun a_39_23 () U)
(declare-fun a_39_24 () U)
(declare-fun a_39_25 () U)
(declare-fun a_39_26 () U)
(declare-fun a_39_27 () U)
(declare-fun a_39_28 () U)
(declare-fun a_39_29 () U)
(declare-fun a_39_30 () U)
(declare-fun a_39_31 () U)
(declare-fun a_39_32 () U)
(declare-fun a_39_33 () U)
(declare-fun a_39_34 () U)
(declare-fun a_39_35 () U)
(declare-fun a_39_36 () U)
(declare-fun a_39_37 () U)
(declare-fun a_39_38 () U)
(declare-fun a_39_39 () U)
(assert (or (or (and (or (not x_0_0) (not x_0_1) (not x_0_2)) (or x_0_0 (not x_0_1) (not x_0_2)) (or (not x_0_0) x_0_1 (not x_0_2)) (or x_0_0 x_0_1 (not x_0_2)) (or (not x_0_0) (not x_0_1) x_0_2) (or x_0_0 (not x_0_1) x_0_2) (or (not x_0_0) x_0_1 x_0_2) (or x_0_0 x_0_1 x_0_2))) (distinct a_0_0 a_0_1 a_0_2 a_0_3 a_0_4 a_0_5 a_0_6 a_0_7 a_0_8 a_0_9 a_0_10 a_0_11 a_0_12 a_0_13 a_0_14 a_0_15 a_0_16 a_0_17 a_0_18 a_0_19 a_0_20 a_0_21 a_0_22 a_0_23 a_0_24 a_0_25 a_0_26 a_0_27 a_0_28 a_0_29 a_0_30 a_0_31 a_0_32 a_0_33 a_0_34 a_0_35 a_0_36 a_0_37 a_0_38 a_0_39)))
(assert (or (or (and (or (not x_1_0) (not x_1_1) (not x_1_2)) (or x_1_0 (not x_1_1) (not x_1_2)) (or (not x_1_0) x_1_1 (not x_1_2)) (or x_1_0 x_1_1 (not x_1_2)) (or (not x_1_0) (not x_1_1) x_1_2) (or x_1_0 (not x_1_1) x_1_2) (or (not x_1_0) x_1_1 x_1_2) (or x_1_0 x_1_1 x_1_2))) (distinct a_1_0 a_1_1 a_1_2 a_1_3 a_1_4 a_1_5 a_1_6 a_1_7 a_1_8 a_1_9 a_1_10 a_1_11 a_1_12 a_1_13 a_1_14 a_1_15 a_1_16 a_1_17 a_1_18 a_1_19 a_1_20 a_1_21 a_1_22 a_1_23 a_1_24 a_1_25 a_1_26 a_1_27 a_1_28 a_1_29 a_1_30 a_1_31 a_1_32 a_1_33 a_1_34 a_1_35 a_1_36 a_1_37 a_1_38 a_1_39)))
(assert (or (or (and (or (not x_2_0) (not x_2_1) (not x_2_2)) (or x_2_0 (not x_2_1) (not x_2_2)) (or (not x_2_0) x_2_1 (not x_2_2)) (or x_2_0 x_2_1 (not x_2_2)) (or (not x_2_0) (not x_2_1) x_2_2) (or x_2_0 (not x_2_1) x_2_2) (or (not x_2_0) x_2_1 x_2_2) (or x_2_0 x_2_1 x_2_2))) (distinct a_2_0 a_2_1 a_2_2 a_2_3 a_2_4 a_2_5 a_2_6 a_2_7 a_2_8 a_2_9 a_2_10 a_2_11 a_2_12 a_2_13 a_2_14 a_2_15 a_2_16 a_2_17 a_2_18 a_2_19 a_2_20 a_2_21 a_2_22 a_2_23 a_2_24 a_2_25 a_2_26 a_2_27 a_2_28 a_2_29 a_2_30 a_2_31 a_2_32 a_2_33 a_2_34 a_2_35 a_2_36 a_2_37 a_2_38 a_2_39)))
(assert (or (or (and (or (not x_3_0) (not x_3_1) (not x_3_2)) (or x_3_0 (not x_3_1) (not x_3_2)) (or (not x_3_0) x_3_1 (not x_3_2)) (or x_3_0 x_3_1 (not x_3_2)) (or (not x_3_0) (not x_3_1) x_3_2) (or x_3_0 (not x_3_1) x_3_2) (or (not x_3_0) x_3_1 x_3_2) (or x_3_0 x_3_1 x_3_2))) (distinct a_3_0 a_3_1 a_3_2 a_3_3 a_3_4 a_3_5 a_3_6 a_3_7 a_3_8 a_3_9 a_3_10 a_3_11 a_3_12 a_3_13 a_3_14 a_3_15 a_3_16 a_3_17 a_3_18 a_3_19 a_3_20 a_3_21 a_3_22 a_3_23 a_3_24 a_3_25 a_3_26 a_3_27 a_3_28 a_3_29 a_3_30 a_3_31 a_3_32 a_3_33 a_3_34 a_3_35 a_3_36 a_3_37 a_3_38 a_3_39)))
(assert (or (or (and (or (not x_4_0) (not x_4_1) (not x_4_2)) (or x_4_0 (not x_4_1) (not x_4_2)) (or (not x_4_0) x_4_1 (not x_4_2)) (or x_4_0 x_4_1 (not x_4_2)) (or (not x_4_0) (not x_4_1) x_4_2) (or x_4_0 (not x_4_1) x_4_2) (or (not x_4_0) x_4_1 x_4_2) (or x_4_0 x_4_1 x_4_2))) (distinct a_4_0 a_4_1 a_4_2 a_4_3 a_4_4 a_4_5 a_4_6 a_4_7 a_4_8 a_4_9 a_4_10 a_4_11 a_4_12 a_4_13 a_4_14 a_4_15 a_4_16 a_4_17 a_4_18 a_4_19 a_4_20 a_4_21 a_4_22 a_4_23 a_4_24 a_4_25 a_4_26 a_4_27 a_4_28 a_4_29 a_4_30 a_4_31 a_4_32 a_4_33 a_4_34 a_4_35 a_4_36 a_4_37 a_4_38 a_4_39)))
(assert (or (or (and (or (not x_5_0) (not x_5_1) (not x_5_2)) (or x_5_0 (not x_5_1) (not x_5_2)) (or (not x_5_0) x_5_1 (not x_5_2)) (or x_5_0 x_5_1 (not x_5_2)) (or (not x_5_0) (not x_5_1) x_5_2) (or x_5_0 (not x_5_1) x_5_2) (or (not x_5_0) x_5_1 x_5_2) (or x_5_0 x_5_1 x_5_2))) (distinct a_5_0 a_5_1 a_5_2 a_5_3 a_5_4 a_5_5 a_5_6 a_5_7 a_5_8 a_5_9 a_5_10 a_5_11 a_5_12 a_5_13 a_5_14 a_5_15 a_5_16 a_5_17 a_5_18 a_5_19 a_5_20 a_5_21 a_5_22 a_5_23 a_5_24 a_5_25 a_5_26 a_5_27 a_5_28 a_5_29 a_5_30 a_5_31 a_5_32 a_5_33 a_5_34 a_5_35 a_5_36 a_5_37 a_5_38 a_5_39)))
(assert (or (or (and (or (not x_6_0) (not x_6_1) (not x_6_2)) (or x_6_0 (not x_6_1) (not x_6_2)) (or (not x_6_0) x_6_1 (not x_6_2)) (or x_6_0 x_6_1 (not x_6_2)) (or (not x_6_0) (not x_6_1) x_6_2) (or x_6_0 (not x_6_1) x_6_2) (or (not x_6_0) x_6_1 x_6_2) (or x_6_0 x_6_1 x_6_2))) (distinct a_6_0 a_6_1 a_6_2 a_6_3 a_6_4 a_6_5 a_6_6 a_6_7 a_6_8 a_6_9 a_6_10 a_6_11 a_6_12 a_6_13 a_6_14 a_6_15 a_6_16 a_6_17 a_6_18 a_6_19 a_6_20 a_6_21 a_6_22 a_6_23 a_6_24 a_6_25 a_6_26 a_6_27 a_6_28 a_6_29 a_6_30 a_6_31 a_6_32 a_6_33 a_6_34 a_6_35 a_6_36 a_6_37 a_6_38 a_6_39)))
(assert (or (or (and (or (not x_7_0) (not x_7_1) (not x_7_2)) (or x_7_0 (not x_7_1) (not x_7_2)) (or (not x_7_0) x_7_1 (not x_7_2)) (or x_7_0 x_7_1 (not x_7_2)) (or (not x_7_0) (not x_7_1) x_7_2) (or x_7_0 (not x_7_1) x_7_2) (or (not x_7_0) x_7_1 x_7_2) (or x_7_0 x_7_1 x_7_2))) (distinct a_7_0 a_7_1 a_7_2 a_7_3 a_7_4 a_7_5 a_7_6 a_7_7 a_7_8 a_7_9 a_7_10 a_7_11 a_7_12 a_7_13 a_7_14 a_7_15 a_7_16 a_7_17 a_7_18 a_7_19 a_7_20 a_7_21 a_7_22 a_7_23 a_7_24 a_7_25 a_7_26 a_7_27 a_7_28 a_7_29 a_7_30 a_7_31 a_7_32 a_7_33 a_7_34 a_7_35 a_7_36 a_7_37 a_7_38 a_7_39)))
(assert (or (or (and (or (not x_8_0) (not x_8_1) (not x_8_2)) (or x_8_0 (not x_8_1) (not x_8_2)) (or (not x_8_0) x_8_1 (not x_8_2)) (or x_8_0 x_8_1 (not x_8_2)) (or (not x_8_0) (not x_8_1) x_8_2) (or x_8_0 (not x_8_1) x_8_2) (or (not x_8_0) x_8_1 x_8_2) (or x_8_0 x_8_1 x_8_2))) (distinct a_8_0 a_8_1 a_8_2 a_8_3 a_8_4 a_8_5 a_8_6 a_8_7 a_8_8 a_8_9 a_8_10 a_8_11 a_8_12 a_8_13 a_8_14 a_8_15 a_8_16 a_8_17 a_8_18 a_8_19 a_8_20 a_8_21 a_8_22 a_8_23 a_8_24 a_8_25 a_8_26 a_8_27 a_8_28 a_8_29 a_8_30 a_8_31 a_8_32 a_8_33 a_8_34 a_8_35 a_8_36 a_8_37 a_8_38 a_8_39)))
(assert (or (or (and (or (not x_9_0) (not x_9_1) (not x_9_2)) (or x_9_0 (not x_9_1) (not x_9_2)) (or (not x_9_0) x_9_1 (not x_9_2)) (or x_9_0 x_9_1 (not x_9_2)) (or (not x_9_0) (not x_9_1) x_9_2) (or x_9_0 (not x_9_1) x_9_2) (or (not x_9_0) x_9_1 x_9_2) (or x_9_0 x_9_1 x_9_2))) (distinct a_9_0 a_9_1 a_9_2 a_9_3 a_9_4 a_9_5 a_9_6 a_9_7 a_9_8 a_9_9 a_9_10 a_9_11 a_9_12 a_9_13 a_9_14 a_9_15 a_9_16 a_9_17 a_9_18 a_9_19 a_9_20 a_9_21 a_9_22 a_9_23 a_9_24 a_9_25 a_9_26 a_9_27 a_9_28 a_9_29 a_9_30 a_9_31 a_9_32 a_9_33 a_9_34 a_9_35 a_9_36 a_9_37 a_9_38 a_9_39)))
(assert (or (or (and (or (not x_10_0) (not x_10_1) (not x_10_2)) (or x_10_0 (not x_10_1) (not x_10_2)) (or (not x_10_0) x_10_1 (not x_10_2)) (or x_10_0 x_10_1 (not x_10_2)) (or (not x_10_0) (not x_10_1) x_10_2) (or x_10_0 (not x_10_1) x_10_2) (or (not x_10_0) x_10_1 x_10_2) (or x_10_0 x_10_1 x_10_2))) (distinct a_10_0 a_10_1 a_10_2 a_10_3 a_10_4 a_10_5 a_10_6 a_10_7 a_10_8 a_10_9 a_10_10 a_10_11 a_10_12 a_10_13 a_10_14 a_10_15 a_10_16 a_10_17 a_10_18 a_10_19 a_10_20 a_10_21 a_10_22 a_10_23 a_10_24 a_10_25 a_10_26 a_10_27 a_10_28 a_10_29 a_10_30 a_10_31 a_10_32 a_10_33 a_10_34 a_10_35 a_10_36 a_10_37 a_10_38 a_10_39)))
(assert (or (or (and (or (not x_11_0) (not x_11_1) (not x_11_2)) (or x_11_0 (not x_11_1) (not x_11_2)) (or (not x_11_0) x_11_1 (not x_11_2)) (or x_11_0 x_11_1 (not x_11_2)) (or (not x_11_0) (not x_11_1) x_11_2) (or x_11_0 (not x_11_1) x_11_2) (or (not x_11_0) x_11_1 x_11_2) (or x_11_0 x_11_1 x_11_2))) (distinct a_11_0 a_11_1 a_11_2 a_11_3 a_11_4 a_11_5 a_11_6 a_11_7 a_11_8 a_11_9 a_11_10 a_11_11 a_11_12 a_11_13 a_11_14 a_11_15 a_11_16 a_11_17 a_11_18 a_11_19 a_11_20 a_11_21 a_11_22 a_11_23 a_11_24 a_11_25 a_11_26 a_11_27 a_11_28 a_11_29 a_11_30 a_11_31 a_11_32 a_11_33 a_11_34 a_11_35 a_11_36 a_11_37 a_11_38 a_11_39)))
(assert (or (or (and (or (not x_12_0) (not x_12_1) (not x_12_2)) (or x_12_0 (not x_12_1) (not x_12_2)) (or (not x_12_0) x_12_1 (not x_12_2)) (or x_12_0 x_12_1 (not x_12_2)) (or (not x_12_0) (not x_12_1) x_12_2) (or x_12_0 (not x_12_1) x_12_2) (or (not x_12_0) x_12_1 x_12_2) (or x_12_0 x_12_1 x_12_2))) (distinct a_12_0 a_12_1 a_12_2 a_12_3 a_12_4 a_12_5 a_12_6 a_12_7 a_12_8 a_12_9 a_12_10 a_12_11 a_12_12 a_12_13 a_12_14 a_12_15 a_12_16 a_12_17 a_12_18 a_12_19 a_12_20 a_12_21 a_12_22 a_12_23 a_12_24 a_12_25 a_12_26 a_12_27 a_12_28 a_12_29 a_12_30 a_12_31 a_12_32 a_12_33 a_12_34 a_12_35 a_12_36 a_12_37 a_12_38 a_12_39)))
(assert (or (or (and (or (not x_13_0) (not x_13_1) (not x_13_2)) (or x_13_0 (not x_13_1) (not x_13_2)) (or (not x_13_0) x_13_1 (not x_13_2)) (or x_13_0 x_13_1 (not x_13_2)) (or (not x_13_0) (not x_13_1) x_13_2) (or x_13_0 (not x_13_1) x_13_2) (or (not x_13_0) x_13_1 x_13_2) (or x_13_0 x_13_1 x_13_2))) (distinct a_13_0 a_13_1 a_13_2 a_13_3 a_13_4 a_13_5 a_13_6 a_13_7 a_13_8 a_13_9 a_13_10 a_13_11 a_13_12 a_13_13 a_13_14 a_13_15 a_13_16 a_13_17 a_13_18 a_13_19 a_13_20 a_13_21 a_13_22 a_13_23 a_13_24 a_13_25 a_13_26 a_13_27 a_13_28 a_13_29 a_13_30 a_13_31 a_13_32 a_13_33 a_13_34 a_13_35 a_13_36 a_13_37 a_13_38 a_13_39)))
(assert (or (or (and (or (not x_14_0) (not x_14_1) (not x_14_2)) (or x_14_0 (not x_14_1) (not x_14_2)) (or (not x_14_0) x_14_1 (not x_14_2)) (or x_14_0 x_14_1 (not x_14_2)) (or (not x_14_0) (not x_14_1) x_14_2) (or x_14_0 (not x_14_1) x_14_2) (or (not x_14_0) x_14_1 x_14_2) (or x_14_0 x_14_1 x_14_2))) (distinct a_14_0 a_14_1 a_14_2 a_14_3 a_14_4 a_14_5 a_14_6 a_14_7 a_14_8 a_14_9 a_14_10 a_14_11 a_14_12 a_14_13 a_14_14 a_14_15 a_14_16 a_14_17 a_14_18 a_14_19 a_14_20 a_14_21 a_14_22 a_14_23 a_14_24 a_14_25 a_14_26 a_14_27 a_14_28 a_14_29 a_14_30 a_14_31 a_14_32 a_14_33 a_14_34 a_14_35 a_14_36 a_14_37 a_14_38 a_14_39)))
(assert (or (or (and (or (not x_15_0) (not x_15_1) (not x_15_2)) (or x_15_0 (not x_15_1) (not x_15_2)) (or (not x_15_0) x_15_1 (not x_15_2)) (or x_15_0 x_15_1 (not x_15_2)) (or (not x_15_0) (not x_15_1) x_15_2) (or x_15_0 (not x_15_1) x_15_2) (or (not x_15_0) x_15_1 x_15_2) (or x_15_0 x_15_1 x_15_2))) (distinct a_15_0 a_15_1 a_15_2 a_15_3 a_15_4 a_15_5 a_15_6 a_15_7 a_15_8 a_15_9 a_15_10 a_15_11 a_15_12 a_15_13 a_15_14 a_15_15 a_15_16 a_15_17 a_15_18 a_15_19 a_15_20 a_15_21 a_15_22 a_15_23 a_15_24 a_15_25 a_15_26 a_15_27 a_15_28 a_15_29 a_15_30 a_15_31 a_15_32 a_15_33 a_15_34 a_15_35 a_15_36 a_15_37 a_15_38 a_15_39)))
(assert (or (or (and (or (not x_16_0) (not x_16_1) (not x_16_2)) (or x_16_0 (not x_16_1) (not x_16_2)) (or (not x_16_0) x_16_1 (not x_16_2)) (or x_16_0 x_16_1 (not x_16_2)) (or (not x_16_0) (not x_16_1) x_16_2) (or x_16_0 (not x_16_1) x_16_2) (or (not x_16_0) x_16_1 x_16_2) (or x_16_0 x_16_1 x_16_2))) (distinct a_16_0 a_16_1 a_16_2 a_16_3 a_16_4 a_16_5 a_16_6 a_16_7 a_16_8 a_16_9 a_16_10 a_16_11 a_16_12 a_16_13 a_16_14 a_16_15 a_16_16 a_16_17 a_16_18 a_16_19 a_16_20 a_16_21 a_16_22 a_16_23 a_16_24 a_16_25 a_16_26 a_16_27 a_16_28 a_16_29 a_16_30 a_16_31 a_16_32 a_16_33 a_16_34 a_16_35 a_16_36 a_16_37 a_16_38 a_16_39)))
(assert (or (or (and (or (not x_17_0) (not x_17_1) (not x_17_2)) (or x_17_0 (not x_17_1) (not x_17_2)) (or (not x_17_0) x_17_1 (not x_17_2)) (or x_17_0 x_17_1 (not x_17_2)) (or (not x_17_0) (not x_17_1) x_17_2) (or x_17_0 (not x_17_1) x_17_2) (or (not x_17_0) x_17_1 x_17_2) (or x_17_0 x_17_1 x_17_2))) (distinct a_17_0 a_17_1 a_17_2 a_17_3 a_17_4 a_17_5 a_17_6 a_17_7 a_17_8 a_17_9 a_17_10 a_17_11 a_17_12 a_17_13 a_17_14 a_17_15 a_17_16 a_17_17 a_17_18 a_17_19 a_17_20 a_17_21 a_17_22 a_17_23 a_17_24 a_17_25 a_17_26 a_17_27 a_17_28 a_17_29 a_17_30 a_17_31 a_17_32 a_17_33 a_17_34 a_17_35 a_17_36 a_17_37 a_17_38 a_17_39)))
(assert (or (or (and (or (not x_18_0) (not x_18_1) (not x_18_2)) (or x_18_0 (not x_18_1) (not x_18_2)) (or (not x_18_0) x_18_1 (not x_18_2)) (or x_18_0 x_18_1 (not x_18_2)) (or (not x_18_0) (not x_18_1) x_18_2) (or x_18_0 (not x_18_1) x_18_2) (or (not x_18_0) x_18_1 x_18_2) (or x_18_0 x_18_1 x_18_2))) (distinct a_18_0 a_18_1 a_18_2 a_18_3 a_18_4 a_18_5 a_18_6 a_18_7 a_18_8 a_18_9 a_18_10 a_18_11 a_18_12 a_18_13 a_18_14 a_18_15 a_18_16 a_18_17 a_18_18 a_18_19 a_18_20 a_18_21 a_18_22 a_18_23 a_18_24 a_18_25 a_18_26 a_18_27 a_18_28 a_18_29 a_18_30 a_18_31 a_18_32 a_18_33 a_18_34 a_18_35 a_18_36 a_18_37 a_18_38 a_18_39)))
(assert (or (or (and (or (not x_19_0) (not x_19_1) (not x_19_2)) (or x_19_0 (not x_19_1) (not x_19_2)) (or (not x_19_0) x_19_1 (not x_19_2)) (or x_19_0 x_19_1 (not x_19_2)) (or (not x_19_0) (not x_19_1) x_19_2) (or x_19_0 (not x_19_1) x_19_2) (or (not x_19_0) x_19_1 x_19_2) (or x_19_0 x_19_1 x_19_2))) (distinct a_19_0 a_19_1 a_19_2 a_19_3 a_19_4 a_19_5 a_19_6 a_19_7 a_19_8 a_19_9 a_19_10 a_19_11 a_19_12 a_19_13 a_19_14 a_19_15 a_19_16 a_19_17 a_19_18 a_19_19 a_19_20 a_19_21 a_19_22 a_19_23 a_19_24 a_19_25 a_19_26 a_19_27 a_19_28 a_19_29 a_19_30 a_19_31 a_19_32 a_19_33 a_19_34 a_19_35 a_19_36 a_19_37 a_19_38 a_19_39)))
(assert (or (or (and (or (not x_20_0) (not x_20_1) (not x_20_2)) (or x_20_0 (not x_20_1) (not x_20_2)) (or (not x_20_0) x_20_1 (not x_20_2)) (or x_20_0 x_20_1 (not x_20_2)) (or (not x_20_0) (not x_20_1) x_20_2) (or x_20_0 (not x_20_1) x_20_2) (or (not x_20_0) x_20_1 x_20_2) (or x_20_0 x_20_1 x_20_2))) (distinct a_20_0 a_20_1 a_20_2 a_20_3 a_20_4 a_20_5 a_20_6 a_20_7 a_20_8 a_20_9 a_20_10 a_20_11 a_20_12 a_20_13 a_20_14 a_20_15 a_20_16 a_20_17 a_20_18 a_20_19 a_20_20 a_20_21 a_20_22 a_20_23 a_20_24 a_20_25 a_20_26 a_20_27 a_20_28 a_20_29 a_20_30 a_20_31 a_20_32 a_20_33 a_20_34 a_20_35 a_20_36 a_20_37 a_20_38 a_20_39)))
(assert (or (or (and (or (not x_21_0) (not x_21_1) (not x_21_2)) (or x_21_0 (not x_21_1) (not x_21_2)) (or (not x_21_0) x_21_1 (not x_21_2)) (or x_21_0 x_21_1 (not x_21_2)) (or (not x_21_0) (not x_21_1) x_21_2) (or x_21_0 (not x_21_1) x_21_2) (or (not x_21_0) x_21_1 x_21_2) (or x_21_0 x_21_1 x_21_2))) (distinct a_21_0 a_21_1 a_21_2 a_21_3 a_21_4 a_21_5 a_21_6 a_21_7 a_21_8 a_21_9 a_21_10 a_21_11 a_21_12 a_21_13 a_21_14 a_21_15 a_21_16 a_21_17 a_21_18 a_21_19 a_21_20 a_21_21 a_21_22 a_21_23 a_21_24 a_21_25 a_21_26 a_21_27 a_21_28 a_21_29 a_21_30 a_21_31 a_21_32 a_21_33 a_21_34 a_21_35 a_21_36 a_21_37 a_21_38 a_21_39)))
(assert (or (or (and (or (not x_22_0) (not x_22_1) (not x_22_2)) (or x_22_0 (not x_22_1) (not x_22_2)) (or (not x_22_0) x_22_1 (not x_22_2)) (or x_22_0 x_22_1 (not x_22_2)) (or (not x_22_0) (not x_22_1) x_22_2) (or x_22_0 (not x_22_1) x_22_2) (or (not x_22_0) x_22_1 x_22_2) (or x_22_0 x_22_1 x_22_2))) (distinct a_22_0 a_22_1 a_22_2 a_22_3 a_22_4 a_22_5 a_22_6 a_22_7 a_22_8 a_22_9 a_22_10 a_22_11 a_22_12 a_22_13 a_22_14 a_22_15 a_22_16 a_22_17 a_22_18 a_22_19 a_22_20 a_22_21 a_22_22 a_22_23 a_22_24 a_22_25 a_22_26 a_22_27 a_22_28 a_22_29 a_22_30 a_22_31 a_22_32 a_22_33 a_22_34 a_22_35 a_22_36 a_22_37 a_22_38 a_22_39)))
(assert (or (or (and (or (not x_23_0) (not x_23_1) (not x_23_2)) (or x_23_0 (not x_23_1) (not x_23_2)) (or (not x_23_0) x_23_1 (not x_23_2)) (or x_23_0 x_23_1 (not x_23_2)) (or (not x_23_0) (not x_23_1) x_23_2) (or x_23_0 (not x_23_1) x_23_2) (or (not x_23_0) x_23_1 x_23_2) (or x_23_0 x_23_1 x_23_2))) (distinct a_23_0 a_23_1 a_23_2 a_23_3 a_23_4 a_23_5 a_23_6 a_23_7 a_23_8 a_23_9 a_23_10 a_23_11 a_23_12 a_23_13 a_23_14 a_23_15 a_23_16 a_23_17 a_23_18 a_23_19 a_23_20 a_23_21 a_23_22 a_23_23 a_23_24 a_23_25 a_23_26 a_23_27 a_23_28 a_23_29 a_23_30 a_23_31 a_23_32 a_23_33 a_23_34 a_23_35 a_23_36 a_23_37 a_23_38 a_23_39)))
(assert (or (or (and (or (not x_24_0) (not x_24_1) (not x_24_2)) (or x_24_0 (not x_24_1) (not x_24_2)) (or (not x_24_0) x_24_1 (not x_24_2)) (or x_24_0 x_24_1 (not x_24_2)) (or (not x_24_0) (not x_24_1) x_24_2) (or x_24_0 (not x_24_1) x_24_2) (or (not x_24_0) x_24_1 x_24_2) (or x_24_0 x_24_1 x_24_2))) (distinct a_24_0 a_24_1 a_24_2 a_24_3 a_24_4 a_24_5 a_24_6 a_24_7 a_24_8 a_24_9 a_24_10 a_24_11 a_24_12 a_24_13 a_24_14 a_24_15 a_24_16 a_24_17 a_24_18 a_24_19 a_24_20 a_24_21 a_24_22 a_24_23 a_24_24 a_24_25 a_24_26 a_24_27 a_24_28 a_24_29 a_24_30 a_24_31 a_24_32 a_24_33 a_24_34 a_24_35 a_24_36 a_24_37 a_24_38 a_24_39)))
(assert (or (or (and (or (not x_25_0) (not x_25_1) (not x_25_2)) (or x_25_0 (not x_25_1) (not x_25_2)) (or (not x_25_0) x_25_1 (not x_25_2)) (or x_25_0 x_25_1 (not x_25_2)) (or (not x_25_0) (not x_25_1) x_25_2) (or x_25_0 (not x_25_1) x_25_2) (or (not x_25_0) x_25_1 x_25_2) (or x_25_0 x_25_1 x_25_2))) (distinct a_25_0 a_25_1 a_25_2 a_25_3 a_25_4 a_25_5 a_25_6 a_25_7 a_25_8 a_25_9 a_25_10 a_25_11 a_25_12 a_25_13 a_25_14 a_25_15 a_25_16 a_25_17 a_25_18 a_25_19 a_25_20 a_25_21 a_25_22 a_25_23 a_25_24 a_25_25 a_25_26 a_25_27 a_25_28 a_25_29 a_25_30 a_25_31 a_25_32 a_25_33 a_25_34 a_25_35 a_25_36 a_25_37 a_25_38 a_25_39)))
(assert (or (or (and (or (not x_26_0) (not x_26_1) (not x_26_2)) (or x_26_0 (not x_26_1) (not x_26_2)) (or (not x_26_0) x_26_1 (not x_26_2)) (or x_26_0 x_26_1 (not x_26_2)) (or (not x_26_0) (not x_26_1) x_26_2) (or x_26_0 (not x_26_1) x_26_2) (or (not x_26_0) x_26_1 x_26_2) (or x_26_0 x_26_1 x_26_2))) (distinct a_26_0 a_26_1 a_26_2 a_26_3 a_26_4 a_26_5 a_26_6 a_26_7 a_26_8 a_26_9 a_26_10 a_26_11 a_26_12 a_26_13 a_26_14 a_26_15 a_26_16 a_26_17 a_26_18 a_26_19 a_26_20 a_26_21 a_26_22 a_26_23 a_26_24 a_26_25 a_26_26 a_26_27 a_26_28 a_26_29 a_26_30 a_26_31 a_26_32 a_26_33 a_26_34 a_26_35 a_26_36 a_26_37 a_26_38 a_26_39)))
(assert (or (or (and (or (not x_27_0) (not x_27_1) (not x_27_2)) (or x_27_0 (not x_27_1) (not x_27_2)) (or (not x_27_0) x_27_1 (not x_27_2)) (or x_27_0 x_27_1 (not x_27_2)) (or (not x_27_0) (not x_27_1) x_27_2) (or x_27_0 (not x_27_1) x_27_2) (or (not x_27_0) x_27_1 x_27_2) (or x_27_0 x_27_1 x_27_2))) (distinct a_27_0 a_27_1 a_27_2 a_27_3 a_27_4 a_27_5 a_27_6 a_27_7 a_27_8 a_27_9 a_27_10 a_27_11 a_27_12 a_27_13 a_27_14 a_27_15 a_27_16 a_27_17 a_27_18 a_27_19 a_27_20 a_27_21 a_27_22 a_27_23 a_27_24 a_27_25 a_27_26 a_27_27 a_27_28 a_27_29 a_27_30 a_27_31 a_27_32 a_27_33 a_27_34 a_27_35 a_27_36 a_27_37 a_27_38 a_27_39)))
(assert (or (or (and (or (not x_28_0) (not x_28_1) (not x_28_2)) (or x_28_0 (not x_28_1) (not x_28_2)) (or (not x_28_0) x_28_1 (not x_28_2)) (or x_28_0 x_28_1 (not x_28_2)) (or (not x_28_0) (not x_28_1) x_28_2) (or x_28_0 (not x_28_1) x_28_2) (or (not x_28_0) x_28_1 x_28_2) (or x_28_0 x_28_1 x_28_2))) (distinct a_28_0 a_28_1 a_28_2 a_28_3 a_28_4 a_28_5 a_28_6 a_28_7 a_28_8 a_28_9 a_28_10 a_28_11 a_28_12 a_28_13 a_28_14 a_28_15 a_28_16 a_28_17 a_28_18 a_28_19 a_28_20 a_28_21 a_28_22 a_28_23 a_28_24 a_28_25 a_28_26 a_28_27 a_28_28 a_28_29 a_28_30 a_28_31 a_28_32 a_28_33 a_28_34 a_28_35 a_28_36 a_28_37 a_28_38 a_28_39)))
(assert (or (or (and (or (not x_29_0) (not x_29_1) (not x_29_2)) (or x_29_0 (not x_29_1) (not x_29_2)) (or (not x_29_0) x_29_1 (not x_29_2)) (or x_29_0 x_29_1 (not x_29_2)) (or (not x_29_0) (not x_29_1) x_29_2) (or x_29_0 (not x_29_1) x_29_2) (or (not x_29_0) x_29_1 x_29_2) (or x_29_0 x_29_1 x_29_2))) (distinct a_29_0 a_29_1 a_29_2 a_29_3 a_29_4 a_29_5 a_29_6 a_29_7 a_29_8 a_29_9 a_29_10 a_29_11 a_29_12 a_29_13 a_29_14 a_29_15 a_29_16 a_29_17 a_29_18 a_29_19 a_29_20 a_29_21 a_29_22 a_29_23 a_29_24 a_29_25 a_29_26 a_29_27 a_29_28 a_29_29 a_29_30 a_29_31 a_29_32 a_29_33 a_29_34 a_29_35 a_29_36 a_29_37 a_29_38 a_29_39)))
(assert (or (or (and (or (not x_30_0) (not x_30_1) (not x_30_2)) (or x_30_0 (not x_30_1) (not x_30_2)) (or (not x_30_0) x_30_1 (not x_30_2)) (or x_30_0 x_30_1 (not x_30_2)) (or (not x_30_0) (not x_30_1) x_30_2) (or x_30_0 (not x_30_1) x_30_2) (or (not x_30_0) x_30_1 x_30_2) (or x_30_0 x_30_1 x_30_2))) (distinct a_30_0 a_30_1 a_30_2 a_30_3 a_30_4 a_30_5 a_30_6 a_30_7 a_30_8 a_30_9 a_30_10 a_30_11 a_30_12 a_30_13 a_30_14 a_30_15 a_30_16 a_30_17 a_30_18 a_30_19 a_30_20 a_30_21 a_30_22 a_30_23 a_30_24 a_30_25 a_30_26 a_30_27 a_30_28 a_30_29 a_30_30 a_30_31 a_30_32 a_30_33 a_30_34 a_30_35 a_30_36 a_30_37 a_30_38 a_30_39)))
(assert (or (or (and (or (not x_31_0) (not x_31_1) (not x_31_2)) (or x_31_0 (not x_31_1) (not x_31_2)) (or (not x_31_0) x_31_1 (not x_31_2)) (or x_31_0 x_31_1 (not x_31_2)) (or (not x_31_0) (not x_31_1) x_31_2) (or x_31_0 (not x_31_1) x_31_2) (or (not x_31_0) x_31_1 x_31_2) (or x_31_0 x_31_1 x_31_2))) (distinct a_31_0 a_31_1 a_31_2 a_31_3 a_31_4 a_31_5 a_31_6 a_31_7 a_31_8 a_31_9 a_31_10 a_31_11 a_31_12 a_31_13 a_31_14 a_31_15 a_31_16 a_31_17 a_31_18 a_31_19 a_31_20 a_31_21 a_31_22 a_31_23 a_31_24 a_31_25 a_31_26 a_31_27 a_31_28 a_31_29 a_31_30 a_31_31 a_31_32 a_31_33 a_31_34 a_31_35 a_31_36 a_31_37 a_31_38 a_31_39)))
(assert (or (or (and (or (not x_32_0) (not x_32_1) (not x_32_2)) (or x_32_0 (not x_32_1) (not x_32_2)) (or (not x_32_0) x_32_1 (not x_32_2)) (or x_32_0 x_32_1 (not x_32_2)) (or (not x_32_0) (not x_32_1) x_32_2) (or x_32_0 (not x_32_1) x_32_2) (or (not x_32_0) x_32_1 x_32_2) (or x_32_0 x_32_1 x_32_2))) (distinct a_32_0 a_32_1 a_32_2 a_32_3 a_32_4 a_32_5 a_32_6 a_32_7 a_32_8 a_32_9 a_32_10 a_32_11 a_32_12 a_32_13 a_32_14 a_32_15 a_32_16 a_32_17 a_32_18 a_32_19 a_32_20 a_32_21 a_32_22 a_32_23 a_32_24 a_32_25 a_32_26 a_32_27 a_32_28 a_32_29 a_32_30 a_32_31 a_32_32 a_32_33 a_32_34 a_32_35 a_32_36 a_32_37 a_32_38 a_32_39)))
(assert (or (or (and (or (not x_33_0) (not x_33_1) (not x_33_2)) (or x_33_0 (not x_33_1) (not x_33_2)) (or (not x_33_0) x_33_1 (not x_33_2)) (or x_33_0 x_33_1 (not x_33_2)) (or (not x_33_0) (not x_33_1) x_33_2) (or x_33_0 (not x_33_1) x_33_2) (or (not x_33_0) x_33_1 x_33_2) (or x_33_0 x_33_1 x_33_2))) (distinct a_33_0 a_33_1 a_33_2 a_33_3 a_33_4 a_33_5 a_33_6 a_33_7 a_33_8 a_33_9 a_33_10 a_33_11 a_33_12 a_33_13 a_33_14 a_33_15 a_33_16 a_33_17 a_33_18 a_33_19 a_33_20 a_33_21 a_33_22 a_33_23 a_33_24 a_33_25 a_33_26 a_33_27 a_33_28 a_33_29 a_33_30 a_33_31 a_33_32 a_33_33 a_33_34 a_33_35 a_33_36 a_33_37 a_33_38 a_33_39)))
(assert (or (or (and (or (not x_34_0) (not x_34_1) (not x_34_2)) (or x_34_0 (not x_34_1) (not x_34_2)) (or (not x_34_0) x_34_1 (not x_34_2)) (or x_34_0 x_34_1 (not x_34_2)) (or (not x_34_0) (not x_34_1) x_34_2) (or x_34_0 (not x_34_1) x_34_2) (or (not x_34_0) x_34_1 x_34_2) (or x_34_0 x_34_1 x_34_2))) (distinct a_34_0 a_34_1 a_34_2 a_34_3 a_34_4 a_34_5 a_34_6 a_34_7 a_34_8 a_34_9 a_34_10 a_34_11 a_34_12 a_34_13 a_34_14 a_34_15 a_34_16 a_34_17 a_34_18 a_34_19 a_34_20 a_34_21 a_34_22 a_34_23 a_34_24 a_34_25 a_34_26 a_34_27 a_34_28 a_34_29 a_34_30 a_34_31 a_34_32 a_34_33 a_34_34 a_34_35 a_34_36 a_34_37 a_34_38 a_34_39)))
(assert (or (or (and (or (not x_35_0) (not x_35_1) (not x_35_2)) (or x_35_0 (not x_35_1) (not x_35_2)) (or (not x_35_0) x_35_1 (not x_35_2)) (or x_35_0 x_35_1 (not x_35_2)) (or (not x_35_0) (not x_35_1) x_35_2) (or x_35_0 (not x_35_1) x_35_2) (or (not x_35_0) x_35_1 x_35_2) (or x_35_0 x_35_1 x_35_2))) (distinct a_35_0 a_35_1 a_35_2 a_35_3 a_35_4 a_35_5 a_35_6 a_35_7 a_35_8 a_35_9 a_35_10 a_35_11 a_35_12 a_35_13 a_35_14 a_35_15 a_35_16 a_35_17 a_35_18 a_35_19 a_35_20 a_35_21 a_35_22 a_35_23 a_35_24 a_35_25 a_35_26 a_35_27 a_35_28 a_35_29 a_35_30 a_35_31 a_35_32 a_35_33 a_35_34 a_35_35 a_35_36 a_35_37 a_35_38 a_35_39)))
(assert (or (or (and (or (not x_36_0) (not x_36_1) (not x_36_2)) (or x_36_0 (not x_36_1) (not x_36_2)) (or (not x_36_0) x_36_1 (not x_36_2)) (or x_36_0 x_36_1 (not x_36_2)) (or (not x_36_0) (not x_36_1) x_36_2) (or x_36_0 (not x_36_1) x_36_2) (or (not x_36_0) x_36_1 x_36_2) (or x_36_0 x_36_1 x_36_2))) (distinct a_36_0 a_36_1 a_36_2 a_36_3 a_36_4 a_36_5 a_36_6 a_36_7 a_36_8 a_36_9 a_36_10 a_36_11 a_36_12 a_36_13 a_36_14 a_36_15 a_36_16 a_36_17 a_36_18 a_36_19 a_36_20 a_36_21 a_36_22 a_36_23 a_36_24 a_36_25 a_36_26 a_36_27 a_36_28 a_36_29 a_36_30 a_36_31 a_36_32 a_36_33 a_36_34 a_36_35 a_36_36 a_36_37 a_36_38 a_36_39)))
(assert (or (or (and (or (not x_37_0) (not x_37_1) (not x_37_2)) (or x_37_0 (not x_37_1) (not x_37_2)) (or (not x_37_0) x_37_1 (not x_37_2)) (or x_37_0 x_37_1 (not x_37_2)) (or (not x_37_0) (not x_37_1) x_37_2) (or x_37_0 (not x_37_1) x_37_2) (or (not x_37_0) x_37_1 x_37_2) (or x_37_0 x_37_1 x_37_2))) (distinct a_37_0 a_37_1 a_37_2 a_37_3 a_37_4 a_37_5 a_37_6 a_37_7 a_37_8 a_37_9 a_37_10 a_37_11 a_37_12 a_37_13 a_37_14 a_37_15 a_37_16 a_37_17 a_37_18 a_37_19 a_37_20 a_37_21 a_37_22 a_37_23 a_37_24 a_37_25 a_37_26 a_37_27 a_37_28 a_37_29 a_37_30 a_37_31 a_37_32 a_37_33 a_37_34 a_37_35 a_37_36 a_37_37 a_37_38 a_37_39)))
(assert (or (or (and (or (not x_38_0) (not x_38_1) (not x_38_2)) (or x_38_0 (not x_38_1) (not x_38_2)) (or (not x_38_0) x_38_1 (not x_38_2)) (or x_38_0 x_38_1 (not x_38_2)) (or (not x_38_0) (not x_38_1) x_38_2) (or x_38_0 (not x_38_1) x_38_2) (or (not x_38_0) x_38_1 x_38_2) (or x_38_0 x_38_1 x_38_2))) (distinct a_38_0 a_38_1 a_38_2 a_38_3 a_38_4 a_38_5 a_38_6 a_38_7 a_38_8 a_38_9 a_38_10 a_38_11 a_38_12 a_38_13 a_38_14 a_38_15 a_38_16 a_38_17 a_38_18 a_38_19 a_38_20 a_38_21 a_38_22 a_38_23 a_38_24 a_38_25 a_38_26 a_38_27 a_38_28 a_38_29 a_38_30 a_38_31 a_38_32 a_38_33 a_38_34 a_38_35 a_38_36 a_38_37 a_38_38 a_38_39)))
(assert (or (or (and (or (not x_39_0) (not x_39_1) (not x_39_2)) (or x_39_0 (not x_39_1) (not x_39_2)) (or (not x_39_0) x_39_1 (not x_39_2)) (or x_39_0 x_39_1 (not x_39_2)) (or (not x_39_0) (not x_39_1) x_39_2) (or x_39_0 (not x_39_1) x_39_2) (or (not x_39_0) x_39_1 x_39_2) (or x_39_0 x_39_1 x_39_2))) (distinct a_39_0 a_39_1 a_39_2 a_39_3 a_39_4 a_39_5 a_39_6 a_39_7 a_39_8 a_39_9 a_39_10 a_39_11 a_39_12 a_39_13 a_39_14 a_39_15 a_39_16 a_39_17 a_39_18 a_39_19 a_39_20 a_39_21 a_39_22 a_39_23 a_39_24 a_39_25 a_39_26 a_39_27 a_39_28 a_39_29 a_39_30 a_39_31 a_39_32 a_39_33 a_39_34 a_39_35 a_39_36 a_39_37 a_39_38 a_39_39)))
(assert (and (= a_0_0 a_1_0) (= a_1_0 a_2_0) (= a_2_0 a_3_0) (= a_3_0 a_4_0) (= a_4_0 a_5_0) (= a_5_0 a_6_0) (= a_6_0 a_7_0) (= a_7_0 a_8_0) (= a_8_0 a_9_0) (= a_9_0 a_10_0) (= a_10_0 a_11_0) (= a_11_0 a_12_0) (= a_12_0 a_13_0) (= a_13_0 a_14_0) (= a_14_0 a_15_0) (= a_15_0 a_16_0) (= a_16_0 a_17_0) (= a_17_0 a_18_0) (= a_18_0 a_19_0) (= a_19_0 a_20_0) (= a_20_0 a_21_0) (= a_21_0 a_22_0) (= a_22_0 a_23_0) (= a_23_0 a_24_0) (= a_24_0 a_25_0) (= a_25_0 a_26_0) (= a_26_0 a_27_0) (= a_27_0 a_28_0) (= a_28_0 a_29_0) (= a_29_0 a_30_0) (= a_30_0 a_31_0) (= a_31_0 a_32_0) (= a_32_0 a_33_0) (= a_33_0 a_34_0) (= a_34_0 a_35_0) (= a_35_0 a_36_0) (= a_36_0 a_37_0) (= a_37_0 a_38_0) (= a_38_0 a_39_0)))
(check-sat)
